-- 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 body Heap_Model with SPARK_Mode is

   function Used (H : Heap) return Count is (H.Allocated);

   procedure Reset (H : out Heap) is
   begin
      H := (Allocated => 0);
   end Reset;

   procedure Allocate (H : in out Heap; Success : out Boolean) is
   begin
      if H.Allocated < Capacity then
         H.Allocated := H.Allocated + 1;
         Success := True;
      else
         Success := False;
      end if;
   end Allocate;

end Heap_Model;