-- SPARK SUBLEQ Attention — implementation
-- Generated by granite-code:3b via Ollama, hardened

package body Attention
  with SPARK_Mode => On
is

   procedure Compute_Attention (Query  : in     Memory_Address;
                                Key    : in     Memory_Address;
                                Value  : in out Memory_Address;
                                Mem    : in out Memory_Array;
                                Result : out    Triad) is
   begin
      -- No softmax: directly compute address triad from Q/K/V positions
      Mem(Value) := Mem(Value) - Mem(Query);
      Result := (A => Query, B => Key, C => Value);
   end Compute_Attention;

   function SUBLEQ_Step (Mem : in out Memory_Array;
                         T   : Triad) return Memory_Address is
   begin
      Mem(T.B) := Mem(T.B) - Mem(T.A);
      if Mem(T.B) <= 0 then
         return T.C;
      else
         return T.A + 3;
      end if;
   end SUBLEQ_Step;

   procedure Run_Attention_Layer (Mem    : in out Memory_Array;
                                  Heads  : in     Triad_Array;
                                  Output : out    Memory_Address) is
      PC : Memory_Address := 0;
   begin
      for I in Heads'Range loop
         PC := SUBLEQ_Step(Mem, Heads(I));
      end loop;
      Output := PC;
   end Run_Attention_Layer;

end Attention;