File size: 1,343 Bytes
ebed3db | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 | -- 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;
|