| -- 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; | |