From Raw Arrays to Typed Ownership: A Layered Allocator in SPARK

In SPARK, heap pointers are supported through a strict ownership model. The tool enforces that designated data cannot alias - ensuring there is always a single, unique owner for any mutable cell. While restrictive, this policy provides a big advantage for formal verification: because ownership pointers cannot alias, SPARK gets framing almost for free. Modifying a designated object (or a data structure containing ownership pointers) automatically preserves all unrelated objects. A few years ago, I wrote a blog post exploring how to model aliased pointers in SPARK using indices into a global memory array. The takeaway was that while index-based memory modeling is possible, it severely weakens SPARK's framing reasoning and quickly becomes far too heavy in practice.

In embedded, safety-critical applications, standard heap allocation is typically forbidden. Instead, developers often declare a static global array and implement a custom memory pool. But using a plain array introduces the same verification bottleneck: SPARK assumes that any subprogram that modifies an array element might affect all others. This led me to a question: Can we hide the underlying array behind a clean abstraction boundary, giving user code the benefits of SPARK ownership while using a static allocator? I decided to try it out. In this post, I will present the architecture, show how we can combine proven layers with a small trusted boundary, and demonstrate how to build safe, statically-backed ownership in SPARK.

Core Array Allocator (PROVED)

The core array allocator is a generic package that provides fixed-capacity storage: objects live in a static array of equal-sized cells, and allocation returns an index into that array rather than a pointer. The generic package lets the user choose both the object type and the index type of the underlying array. It also takes as parameters the maximum number of elements the allocator can contain and the object size. The fact that the value supplied for the size of the object is consistent with the object type is checked at compile time and produces an error if it fails:

generic
   type Index_Base is range <>;
   type Binary_Object_Type is private;
   Object_Size : Positive;
   --  Size of the object we want to store in byte
   Allocator_Length : Natural := 100;
   --  Maximal number of elements that can be allocated in the buffer 
package Allocator.Base is
   pragma
     Compile_Time_Error
       (Binary_Object_Type'Size /= 8 * Object_Size,
        "Binary_Object_Type should have Object_Size bytes");

The implementation of the allocator is memory-efficient. It reuses the array cells to implement a free list by storing the index of the next free cell directly in the Memory array. This is what the Memory_Cell_Type is used for. It is a record of size Object_Size that contains a field for the next cell in the free list, along with some padding. To read the value of an allocated cell as an object of type Binary_Object_Type, it is necessary to introduce an overlay or an unchecked conversion, like the function To_Object below. Overlays and unchecked conversions are used to reinterpret the bitwise representation of an object as that of another object in Ada and are severely restricted in SPARK, but are allowed. The head of the free list is stored in a separate variable called Free. An optimization is used to avoid initializing the free list by using a negative value to indicate that the remaining cells are free:

   subtype Extended_Index is
     Index_Base'Base
       range Index_Base'Base (-Allocator_Length))
             .. Index_Base'Base (Allocator_Length));
   subtype Index_Type is Extended_Index range 1 .. Extended_Index'Last;

   type Padding_Type is
     array (Positive range 1 .. Object_Size - Extended_Index'Object_Size / 8)
     of Unsigned_8;

   type Memory_Cell_Type is record
      Next    : Extended_Index'Base;
      Padding : Padding_Type;
   end record
   with Alignment => 1;
   --  An object is a byte array of size Object_Size. Use the beginning of the
   --  array to store the index of the next free cell if the object is free. A
   --  negative number stands for the end of the buffer starting at -Next.

   function To_Object is new
     Ada.Unchecked_Conversion
       (Memory_Cell_Type,
        Binary_Object_Type) with Potentially_Invalid;

   Memory : Memory_Type;
   Free   : Extended_Index := (if Allocator_Length = 0 then 0 else -1);
   --  Buffer and first index of the free list. A negative number stands for
   --  the end of the buffer starting at -Free.

To model the allocator, we have introduced two containers: a map from array indices to object values for allocated cells, and a sequence of indices for free cells. The Memory_Cell_Type type is completely abstracted away in the model, and no unchecked conversions are visible:

   package Memory_Index_Maps is new
     SPARK.Containers.Functional.Maps (Index_Type, Binary_Object_Type);
   package Memory_Index_Sequences is new
     SPARK.Containers.Functional.Infinite_Sequences (Index_Type);

   function Allocated_Cells return Memory_Index_Maps.Map
   with
     Ghost,
     Global => (Memory, Free),
     Pre    => Base_Invariant,
     Post   =>
       (for all I of Allocated_Cells'Result =>
          I in 1 .. Extended_Index (Allocator_Length));

   function Free_Cells return Memory_Index_Sequences.Sequence
   with Ghost, Global => (Memory, Free), Pre => Base_Invariant;

Using these models, we have annotated the allocator operations with Platinum-level contracts. Here is an example of how it is expressed for Allocate. In particular, this contract specifies how the other cells are affected by the allocation. As discussed in the introduction, this framing is necessary since the Memory array is shared between the various objects:

   function Allocate (O : Binary_Object_Type) return Index_Type
   with
     Side_Effects,
     Global => (In_Out => (Memory, Free)),
     Pre    => Invariant and then Length (Free_Cells) > 0,
     Post   =>
       Invariant

       --  Allocate does not affect other allocated cells

       and then Allocated_Cells'Old <= Allocated_Cells
       and then
         Keys_Included_Except
           (Allocated_Cells, Allocated_Cells'Old, Allocate'Result)

       --  A new cell is allocated

       and then not Has_Key (Allocated_Cells'Old, Allocate'Result)
       and then Has_Key (Allocated_Cells, Allocate'Result)
       and then Get (Allocated_Cells, Allocate'Result) = O
       and then Length (Allocated_Cells) = Length (Allocated_Cells'Old) + 1

      --  The last cell of the free list has been allocated

       and then Length (Free_Cells) = Length (Free_Cells'Old) - 1
       and then Free_Cells < Free_Cells'Old
       and then Allocate'Result = Get (Free_Cells'Old, Last (Free_Cells'Old));

The implementation of this core library and its contracts can be verified using the Reachability package from SPARKlib, which I presented in a recent blog post. If you are interested, the code can be found in the SPARK testsuite. The file allocator_base.ads contains the core allocator. The code in the test suite is handwritten, but I have checked that agentic AI can generate both the implementation and the proof from the specification using the Reachability library and its lemmas.

Ownership Cell Transformation (UNPROVED)

The core allocator library presented in the previous section is self-contained and can be used as it is. However, as discussed at the beginning of this blog post, it can easily become overly heavy, as memory cells cannot be reasoned with independently. Here, we want to refine the two concrete global objects Free and Memory into separate objects per allocated memory cell, along with a global object for the rest (the free list). We write this new interface in a separate package named Allocator.Ownership_Wrapper. It defines an abstract state called The_Memory for the free list, and an Object_Pointer type for an allocated cell. It uses the Ownership annotation to enforce non-aliasing among allocated cells and to enable reclamation. For an Object_Pointer to be reclaimed, Is_Null shall return True:

package Allocator.Ownership_Wrapper with
    Abstract_State => The_Memory
is

   function Num_Free return Big_Natural
   with Ghost, Global => The_Memory;
  --  Number of free cells in the allocator

   type Object_Pointer is private
   with
     Annotate                  => (GNATprove, Ownership, "Needs_Reclamation"),
     Default_Initial_Condition => Is_Null (Object_Pointer);

   function Is_Null (P : Object_Pointer) return Boolean
   with Annotate => (GNATprove, Ownership, "Is_Reclaimed");

The operations defined on the core allocator can easily be adapted to these new declarations. Operations that affect the free list, such as Allocate, keep a common global reference on The_Memory, whereas those that access only a single cell, such as Deref, are now pure. To preserve efficiency, this library also exports traversal functions Constant_Reference and Reference. Traversal functions are functions that return access to a part of their first parameter. It allows read-only (for Constant_Reference) or read/write (for Reference) access without copies to the object designated by an Object_Pointer.

   function Deref (P : Object_Pointer) return Binary_Object_Type
   with Global => null, Pre => not Is_Null (P);

   function Reference
     (P : in out Object_Pointer) return not null access Binary_Object_Type
   with
     Global => null,
     Pre    => not Is_Null (P),
     Post   =>
       not Is_Null (At_End (P))
       and then At_End (Reference'Result).all = Deref (At_End (P));

   function Allocate (O : Binary_Object_Type) return Object_Pointer
   with
     Side_Effects,
     Global => (In_Out => The_Memory),
     Pre    => Num_Free > 0,
     Post   =>
       Num_Free = Num_Free'Old - 1
       and then not Is_Null (Allocate'Result)
       and then Deref (Allocate'Result) = O;

Unfortunately, while proof supports contract refinement in general (as explained in a previous blog post), state refinement is mostly out of scope for SPARK. As a consequence, the private part and the body of Allocator.Ownership_Wrapper cannot be verified formally. To make their review easier, we have kept their implementation minimal, typically a single call from the core API.

   type Object_Pointer is record
      Index : Extended_Index := 0;
   end record
   with Predicate => Index >= 0;

   function Is_Null (P : Object_Pointer) return Boolean
   is (P.Index = 0);

   function Allocate (O : Binary_Object_Type) return Object_Pointer is
   begin
      return (Index => Allocate (O));
   end Allocate;

The soundness of this approach relies on the fact that this specification is a real refinement of the core specification. In particular, the core allocator’s specification should be enough to ensure that modifying one of the abstract objects that the concrete state is split into cannot affect the others. This can be deduced from the contracts of the core API, which enforce preservation of other cells, along with the ownership annotation on Object_Pointer, which ensures that two allocated objects necessarily have different indexes. Note that currently, it is not possible to define (and prove) a traversal function like Reference that would return a part of a global object - and not of its first parameter. It is left as future work until the language is extended to support it.

Typed & Multi-Pool Layer (PROVED)

The allocator API with ownership presented in the previous section is deliberately small and low-level to keep the unproven wrapper as thin as possible. On top of it, we can now add capabilities to our allocator and have them formally verified by SPARK. In particular, we have looked into two improvements: strong typing and support of objects of different sizes.

The first improvement we have looked into is strong typing. It would be nice to allocate objects of different types with our allocator and ensure they retain their correct types when retrieved. To be able to store typed objects inside an untyped allocator - containing an array of bytes - we need to use type reinterpretation - that is, to reinterpret the bitwise representation of an object of a type as an object of another type. Type reinterpretation in Ada can be done either using an overlay (two objects with the same address) or through an unchecked conversion. Both are supported in SPARK, but with several restrictions. In particular, type reinterpretation cannot be used on pointers. Unfortunately, here we are using traversal functions as accessors for efficiency, so we need a way to reinterpret the value of an access to one type as a value of an access to another type. To address this issue, we can use the package SPARK.Conversions.Access_Conversions that has been added to the SPARKlib recently. It provides conversion functions for access types that rely on type reinterpretation. They contain (ghost) instances of unchecked conversion in their specification, which are used to force the proof tool to make sure that reinterpretation is safe for the designated types. They provide conversion functions for access types, implemented as traversal functions that return a portion of their parameter. The specific flavor shown below supports a target type that may contain invalid values. It requires checking the validity of the conversion result before using it:

   generic
      type Source_Type is private;
      type Target_Type is private;
   package Access_Variable_Conversions_Potentially_Invalid is

      function Target_Logical_Equal (X, Y : Target_Type) return Boolean
      with Ghost => SPARKlib_Full, Annotate => (GNATprove, Logical_Equal);

      function Object_Conversion is new
        Ada.Unchecked_Conversion
          (Source_Type,
           Target_Type) with Potentially_Invalid;
      --  Make sure that it is safe to reinterpret an object of type
      --  Source_Type as a potentially invalid object of type Target_Type.

      function Object_Reverse_Conversion is new
        Ada.Unchecked_Conversion (Target_Type, Source_Type);
      --  Make sure that it is safe to reinterpret an object of type
      --  Target_Type as an object of type Source_Type. This is necessary for
      --  Reference. We cannot support potentially invalid data here, as there
      --  is no way to constrain what can be stored in the borrowed object.

      function Convert_Access
        (Source : not null access Source_Type)
         return not null access Target_Type
      with
        Global => null,
        Pre    =>
          (SPARKlib_Defensive => Object_Conversion (Source.all)'Valid_Scalars),
        Post   =>
          (SPARKlib_Full =>
             (declare
                Target : constant Target_Type :=
                  Object_Conversion (At_End (Source).all)
                with Potentially_Invalid;
              begin
                Target'Valid_Scalars
                and then
                  Target_Logical_Equal
                    (At_End (Convert_Access'Result).all, Target)));

   end Access_Variable_Conversions_Potentially_Invalid;

Since we are using type reinterpretation underneath, our typed allocator can only be used on values that are suitable for unchecked conversions, as defined in SPARK - you can look at the definition if you are interested. This restriction seems acceptable in our context.

The other improvement we have looked into is handling objects of different sizes. Our core array allocator only works for objects of a given size. In the literature, it is common to support allocating contiguous cells to store larger objects, but this is complicated and requires handling fragmentation, so we have not attempted it. Instead, we have decided to use several core allocators with different sizes. Objects of a given type are preferably allocated by the allocator with the smallest object size that fits them, but can be promoted to allocators with a larger object size if needed. The architecture is as follows. The first generic package, named Pools, contains the core allocators with their ownership wrappers. It lets the user choose the maximum number of objects of the five possible raw sizes (4, 8, 16, 32, and 64 bytes) they want to allocate:

--  Outer generic. It creates, hidden in its private part, a five-byte array
--  allocators (cells of 4, 8, 16, 32, and 64 bytes) on top of Allocator.Base +
--  Allocator.Base.Ownership_Wrapper. It exposes only Num_Free_4 .. Num_Free_64:
--  the number of free cells in each bucket (one per size, since the free count
--  is a property of the shared bucket).

generic
   Length_4 : Natural := 0;
   Length_8 : Natural := 0;
   Length_16 : Natural := 0;
   Length_32 : Natural := 0;
   Length_64 : Natural := 0;
package Allocator.Pools with [...] is

   --  Number of free cells in each bucket.

   function Num_Free_4 return Big_Natural
   with Ghost, Global => Memory_4;
   function Num_Free_8 return Big_Natural
   with Ghost, Global => Memory_8;
   function Num_Free_16 return Big_Natural
   with Ghost, Global => Memory_16;
   function Num_Free_32 return Big_Natural
   with Ghost, Global => Memory_32;
   function Num_Free_64 return Big_Natural
   with Ghost, Global => Memory_64;

private

   package Wrapper_4 is new
     Ownership_Wrapper
       (4,
        Length_4,
        Storage_4,
        Integer_16) with Part_Of => Memory_4;
[...]

end;

Then, five generic children of Pools are defined, one per supported raw size. They take as a parameter the type of the objects to allocate - object pointers defined for a given type can only hold objects of this type, which ensures strong typing, along with a boolean that encodes whether promotion, using an allocator with bigger objects, is allowed for this type. It is the user who must decide which generic package to instantiate based on the object's size. It would have been better if this choice could have been done automatically, but the framework doesn’t allow it. Each generic child defines a wrapper for each supported size that fits the object. It contains the object with some padding. The Access_Conversions library is used to convert them to the object type of the raw allocators. The public specification of each generic child provides the same functionalities as the underlying allocators, but for a typed object. Promotion is enabled by using a variant record for the object pointer; the associated raw allocator can be deduced from the pointer kind. As an example, here is the generic child package that can be used to allocate objects with sizes ranging from 5 to 8. Note the contract of Allocate. It uses the recently added Modifies aspect to precisely state which of the global memory objects is modified based on whether the new pointer is promoted:

--  Per-size wrapper for objects whose smallest fitting bucket is 8 bytes.
--  Stores in bucket 8 and, when With_Promotion is True, and bucket 8 is full,
--  transparently promotes to buckets 16, 32, 64. Provides the same API as
--  Allocator.Base.Ownership_Wrapper over the user's Object_Type.
--
--  Object_Bytes is the size of Object_Type in bytes; the user passes it as a
--  static value (it must equal Object_Type'Object_Size / 8, checked at
--  instantiation) and must lie in 5 .. 8 for this wrapper.

generic
   type Object_Type is private;
   Object_Bytes : Positive;
   With_Promotion : Boolean := True;
package Allocator.Pools.Sized_8 with SPARK_Mode is

   pragma
     Compile_Time_Error
       (Object_Bytes /= Object_Type'Object_Size / 8,
        "Object_Bytes is inconsistant with Object_Type");
   pragma Compile_Time_Error (Object_Bytes > 8, "Object_Bytes bigger than 8");
   pragma
     Compile_Time_Error (Object_Bytes <= 4, "Object_Bytes smaller than 4");

   type Object_Pointer is private
   with Default_Initial_Condition => Is_Null (Object_Pointer);

   function Reference
     (P : in out Object_Pointer) return not null access Object_Type
   with
     Global => null,
     Pre    => not Is_Null (P),
     Post   =>
       not Is_Null (At_End (P))
       and then Obj_Eq (At_End (Reference'Result).all, Deref (At_End (P)));

   function Allocate (O : Object_Type) return Object_Pointer
   with
     Side_Effects,
     Global   => (In_Out => (Memory_8, Memory_16, Memory_32, Memory_64)),
     Modifies =>
       (Memory_8 when Num_Free_8 > 0,
        Memory_16 when Num_Free_8 = 0 and Num_Free_16 > 0,
        Memory_32 when Num_Free_8 = 0 and Num_Free_16 = 0 and Num_Free_32 > 0,
        Memory_64 when Num_Free_8 = 0 and Num_Free_16 = 0 and Num_Free_32 = 0),
     Pre      => Num_Free > 0,
     Post     =>
       Num_Free = Num_Free'Old - 1
       and then not Is_Null (Allocate'Result)
       and then Obj_Eq (Deref (Allocate'Result), O);

[...]

private

   --  The object lives in exactly one bucket (or nowhere)
   type Bucket_Kind is (None_Bucket, In_8, In_16, In_32, In_64);

   type Bucket_Pointer (Kind : Bucket_Kind := None_Bucket) is record
      case Kind is
         when None_Bucket =>
            null;
         when In_8 =>
            P8 : Wrapper_8.Object_Pointer;
         when In_16 =>
            P16 : Wrapper_16.Object_Pointer;
         when In_32 =>
            P32 : Wrapper_32.Object_Pointer;
         when In_64 =>
            P64 : Wrapper_64.Object_Pointer;
      end case;
   end record;

[...]
end;

Implementing these features on top of the ownership wrapper was straightforward, and agentic AI did so with minimal guidance. The same work on top of the core allocators would not have allowed for clean abstraction, in particular with respect to typing. The conversions would have had to remain visible in the interface to reason about preserved cells.

Conclusion

Contrary to common belief, formal verification isn't an "all-or-nothing" proposition. In practice, the most pragmatic way to build safe systems software in SPARK is to apply formal proof where it yields the highest return, encapsulating the unprovable gaps behind tight, carefully audited boundaries so the rest of the application can be verified easily and safely.

This post presented a static array allocator tailored for embedded, safety-critical contexts. The core allocator algorithm is fully verified to SPARK Platinum (full functional correctness). To streamline verification of user code, this core is wrapped in a thin layer that hides the backing array and maps raw indices to distinct, owned cells. This wrapper remains unproven because SPARK’s pointer ownership model cannot directly represent dynamic state refinement across array elements. However, because this boundary is minimal and its soundness relies directly on properties proven in the core, auditing it via code review is a low-risk, highly acceptable trade-off. Richer capabilities - such as strong typing and multi-pool memory promotion - are then built on top of this cell abstraction, returning to 100% formal verification in SPARK.

The thin, unproven layer with a carefully designed boundary is quite similar to what is generally necessary when using a library implemented in a language that is not SPARK (C, or full Ada) and does not meet its requirements. The approach presented in this post is original in that it uses the boundary between two parts, both of which are fully verified in SPARK, to introduce abstraction and simplify verification of user code.

There is an example of the allocator described in this blog post in our test suite, a great place to get started if you want to add a static allocator with partial SPARK Platinum proof to your next design.