-- Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
-- SPDX-License-Identifier: LicenseRef-Proprietary
-- Public source visibility does not grant an open-source license. See LICENSE.

package Heap_Model with SPARK_Mode is
   Capacity : constant := 64;
   subtype Index is Natural range 0 .. Capacity - 1;
   subtype Count is Natural range 0 .. Capacity;

   type Heap is private;

   function Used (H : Heap) return Count;

   procedure Reset (H : out Heap)
     with Post => Used (H) = 0;

   procedure Allocate (H : in out Heap; Success : out Boolean)
     with
       Pre  => Used (H) <= Capacity,
       Post =>
         Success = (Used (H'Old) < Capacity) and then
         (if Success then Used (H) = Used (H'Old) + 1
          else Used (H) = Used (H'Old));

private
   type Heap is record
      Allocated : Count := 0;
   end record;
end Heap_Model;