saint-graves/sica-fondt
1
0
Fork 0
mirror of https://github.com/SHOGGOTH-SECTOR/sica-fondt.git synced 2026-09-30 01:15:10 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #4 from SHOGGOTH-SECTOR/claude/sufficiency-assessment-ufuaf4

Browse Source 
Gen.03 organ-systems core: Ada Medium, Soul/Tarot, trust boundary, Hermes MCP bridge
This commit is contained in:
gravermistakes
2026-06-09 19:09:23 -07:00
committed by GitHub
parent ca3e1c4441 b381b780c2
commit f41629b181
25 changed files with 2856 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.github/workflows/ci.yml
+69
View File
@@ -0,0 +1,69 @@
name: Ada CI
# Scheduled only — does NOT run on push or PR. Runs nightly and can be
# triggered by hand from the Actions tab.
on:
schedule:
- cron: "0 6 * * *" # 06:00 UTC daily
workflow_dispatch:
permissions:
contents: read
jobs:
build-and-test:
name: alr build + run tests
runs-on: ubuntu-latest
defaults:
run:
working-directory: mafiabot_core
steps:
- uses: actions/checkout@v4
- name: Set up Alire + GNAT/GPRbuild toolchain
uses: alire-project/setup-alire@v4
with:
toolchain: gnat_native^14 gprbuild
- name: Build (Ada2022 + SPARK + Jorvik)
run: alr --non-interactive build
- name: Run test executables
run: |
set -euo pipefail
fail=0
for t in soul_tests trust_tests cycle_tests config_tests engine_tests; do
if [ -x "bin/$t" ]; then
echo "=== $t ==="
if ! "bin/$t"; then
echo "::error::$t exited non-zero"
fail=1
fi
else
echo "::warning::bin/$t not found (skipped)"
fi
done
exit $fail
prove:
name: gnatprove (informational)
runs-on: ubuntu-latest
# Proofs are not yet expected to fully discharge; surface results without
# blocking. Flip continue-on-error to false once the proof base is green.
continue-on-error: true
defaults:
run:
working-directory: mafiabot_core
steps:
- uses: actions/checkout@v4
- name: Set up Alire
uses: alire-project/setup-alire@v4
with:
toolchain: gnat_native^14 gprbuild
- name: Install gnatprove
run: alr --non-interactive toolchain --select gnatprove || alr --non-interactive with gnatprove || true
- name: Run gnatprove
run: alr --non-interactive exec -- gnatprove -P mafiabot_core.gpr --level=1 --report=fail || true
mafiabot_core/mafiabot_core.gpr
+13 -1
View File
@@ -8,11 +8,23 @@ project Mafiabot_Core is
"src/daemons",
"src/network",
"src/payloads",
"src/types",
"src/config_loader",
"src/trust",
"src/organs/soul",
"src/organs/ada_medium",
"src/protocol",
"config",
"tests");
for Object_Dir use "obj";
for Exec_Dir use "bin";
for Main use ("mafiabot.adb", "engine_tests.adb");
for Main use
("mafiabot.adb",
"engine_tests.adb",
"soul_tests.adb",
"trust_tests.adb",
"cycle_tests.adb",
"config_tests.adb");
package Builder is
for Global_Configuration_Pragmas use "gnat.adc";
mafiabot_core/src/config_loader/config_loader.adb
+164
View File
@@ -0,0 +1,164 @@
package body Config_Loader
with SPARK_Mode => On
is
-- Skip leading/trailing ASCII spaces and tabs in a substring.
procedure Trim_Bounds
(S : in String;
First : in out Positive;
Last : in out Natural)
with Pre => S'First <= First and then Last <= S'Last;
procedure Trim_Bounds
(S : in String;
First : in out Positive;
Last : in out Natural)
is
begin
while First <= Last and then (S (First) = ' ' or else S (First) = ASCII.HT) loop
First := First + 1;
end loop;
while Last >= First and then (S (Last) = ' ' or else S (Last) = ASCII.HT) loop
Last := Last - 1;
end loop;
end Trim_Bounds;
procedure Load_From_Buffer
(Buf : in String;
Store : out Config_Store;
Status : out Operation_Status)
is
Line_Start : Positive := Buf'First;
I : Positive;
Line_End : Natural;
Colon_Pos : Natural;
K_First : Positive;
K_Last : Natural;
V_First : Positive;
V_Last : Natural;
Key_Len : Key_Length;
Val_Len : Val_Length;
begin
Store := (Count => 0,
Entries => (others => (Key => (others => ' '), Key_Len => 0,
Val => (others => ' '), Val_Len => 0)));
Status := OK;
I := Buf'First;
while I <= Buf'Last loop
-- Find end of current line
Line_Start := I;
Line_End := I - 1;
while I <= Buf'Last and then Buf (I) /= ASCII.LF loop
Line_End := I;
I := I + 1;
end loop;
-- Consume newline
if I <= Buf'Last and then Buf (I) = ASCII.LF then
I := I + 1;
end if;
-- Skip blank lines and comments
K_First := Line_Start;
K_Last := Line_End;
Trim_Bounds (Buf, K_First, K_Last);
if K_First > K_Last
or else Buf (K_First) = '#'
then
goto Next_Line;
end if;
-- Find colon separator
Colon_Pos := 0;
for J in K_First .. K_Last loop
if Buf (J) = ':' then
Colon_Pos := J;
exit;
end if;
end loop;
if Colon_Pos = 0 then
goto Next_Line; -- no colon: not a key-value line, skip
end if;
-- Key span
K_First := Line_Start;
K_Last := Colon_Pos - 1;
Trim_Bounds (Buf, K_First, K_Last);
-- Value span
V_First := Colon_Pos + 1;
V_Last := Line_End;
if V_First <= V_Last then
Trim_Bounds (Buf, V_First, V_Last);
end if;
-- Validate lengths
if K_Last < K_First then
goto Next_Line;
end if;
Key_Len := K_Last - K_First + 1;
if Key_Len > Max_Key_Len then
Status := Error_Config;
return;
end if;
if V_Last >= V_First then
Val_Len := V_Last - V_First + 1;
else
Val_Len := 0;
end if;
if Val_Len > Max_Val_Len then
Status := Error_Config;
return;
end if;
-- Check store capacity
if Store.Count = Max_Keys then
Status := Error_Overflow;
return;
end if;
Store.Count := Store.Count + 1;
declare
Idx : constant Entry_Index := Entry_Index (Store.Count);
begin
Store.Entries (Idx).Key_Len := Key_Len;
Store.Entries (Idx).Key (1 .. Key_Len) :=
Buf (K_First .. K_Last);
Store.Entries (Idx).Val_Len := Val_Len;
if Val_Len > 0 then
Store.Entries (Idx).Val (1 .. Val_Len) :=
Buf (V_First .. V_Last);
end if;
end;
<<Next_Line>>
null;
end loop;
end Load_From_Buffer;
function Get_Value
(Store : Config_Store;
Key : String) return Bounded_Text
is
Result : Bounded_Text;
begin
for I in 1 .. Store.Count loop
declare
E : constant Config_Entry := Store.Entries (Entry_Index (I));
begin
if E.Key_Len = Key'Length
and then E.Key (1 .. E.Key_Len) = Key
then
Result.Length := E.Val_Len;
Result.Data (1 .. E.Val_Len) := E.Val (1 .. E.Val_Len);
return Result;
end if;
end;
end loop;
return Result;
end Get_Value;
end Config_Loader;
mafiabot_core/src/config_loader/config_loader.ads
+46
View File
@@ -0,0 +1,46 @@
-- SPARK-safe flat key-value config parser.
-- Reads "key: value" lines; skips blank lines and comments (# prefix).
-- No heap, no exceptions, no finalization — SPARK_Mode On throughout.
with Mafiabot_Types; use Mafiabot_Types;
package Config_Loader
with SPARK_Mode => On
is
Max_Keys : constant := 64;
Max_Key_Len : constant := 128;
Max_Val_Len : constant := 512;
subtype Key_Length is Natural range 0 .. Max_Key_Len;
subtype Val_Length is Natural range 0 .. Max_Val_Len;
type Config_Entry is record
Key : String (1 .. Max_Key_Len) := (others => ' ');
Key_Len : Key_Length := 0;
Val : String (1 .. Max_Val_Len) := (others => ' ');
Val_Len : Val_Length := 0;
end record;
type Entry_Index is range 1 .. Max_Keys;
subtype Entry_Count is Natural range 0 .. Max_Keys;
type Config_Store is record
Entries : array (Entry_Index) of Config_Entry :=
(others => (Key => (others => ' '), Key_Len => 0,
Val => (others => ' '), Val_Len => 0));
Count : Entry_Count := 0;
end record;
-- Parse Buf (a complete file read into a string) into Store.
procedure Load_From_Buffer
(Buf : in String;
Store : out Config_Store;
Status : out Operation_Status)
with Pre => Buf'Length > 0;
-- Retrieve the value for Key; returns empty Bounded_Text if not found.
function Get_Value
(Store : Config_Store;
Key : String) return Bounded_Text;
end Config_Loader;
mafiabot_core/src/mafiabot.adb
+128 -1
View File
@@ -1,4 +1,131 @@
-- NullClaw / AI Mafia Bot Gen.03 — MCP stdio server entry point.
--
-- Speaks JSON-RPC over stdin/stdout so the Hermes Agent harness can mount it
-- as an `mcp_servers` entry. On start it fixes the global Big-3 identity and
-- writes ~/.hermes/SOUL.md, then serves: initialize, tools/list, tools/call.
-- Each tools/call runs the 23-step organ-systems inference cycle, scoped to a
-- session keyed by (uid, channel, server) drawn from the call arguments.
--
-- SPARK_Mode Off: the driver performs I/O and orchestration only — it calls
-- into the SPARK-proven organs (Ada_Medium, Soul.State, Trust_Boundary) and
-- the SPARK_Mode-Off protocol bridge. No proof obligations live here.
pragma SPARK_Mode (Off);
with Mafiabot_Types; use Mafiabot_Types;
with Soul.Tarot;
with Soul.State;
with Ada_Medium;
with Hermes_Protocol;
procedure Mafiabot is
-- Default identity anchors (three distinct Majors). A config-driven Big-3
-- is a follow-up item; these give a stable, valid starting identity.
Default_Big_Three : constant Soul.Tarot.Big_Three :=
(Sun => (Kind => Soul.Tarot.Major, Major_Value => Soul.Tarot.The_Sun),
Moon => (Kind => Soul.Tarot.Major, Major_Value => Soul.Tarot.The_Moon),
Ascendant => (Kind => Soul.Tarot.Major,
Major_Value => Soul.Tarot.SD_Singularity));
procedure Compare (A : Bounded_Text; B : String; Equal : out Boolean) is
begin
Equal := A.Length = B'Length
and then A.Data (1 .. A.Length) = B;
end Compare;
Status : Operation_Status;
Soul_Buf : Bounded_Text;
begin
null;
-- --- Organ init: fix identity, publish SOUL.md ---------------------
Soul.State.Soul_State.Initialize_Big_Three (Default_Big_Three, Status);
if Status /= OK then
return; -- cannot run without a valid identity
end if;
Soul.State.Soul_State.Generate_Soul_MD (Soul_Buf, Status);
if Status = OK then
Hermes_Protocol.Write_Soul_MD (Soul_Buf, Status);
-- A failed SOUL.md write is non-fatal: Hermes can still call tools.
end if;
-- --- MCP serve loop ------------------------------------------------
loop
declare
In_Buf : Hermes_Protocol.JSON_Buffer;
Out_Buf : Hermes_Protocol.JSON_Buffer;
Read_St : Operation_Status;
Id : Bounded_Text;
Method : Bounded_Text;
Is_Init : Boolean;
Is_List : Boolean;
Is_Call : Boolean;
Is_Notif : Boolean;
begin
Hermes_Protocol.Read_Message (In_Buf, Read_St);
exit when Read_St /= OK; -- stdin closed -> shut down
if In_Buf.Length > 0 then -- skip blank lines
Hermes_Protocol.Extract_Raw_Field (In_Buf, "id", Id);
Hermes_Protocol.Extract_Field (In_Buf, "method", Method);
Compare (Method, "initialize", Is_Init);
Compare (Method, "tools/list", Is_List);
Compare (Method, "tools/call", Is_Call);
Compare (Method, "notifications/initialized", Is_Notif);
if Is_Init then
Hermes_Protocol.Make_Init_Response (Id, Out_Buf);
Hermes_Protocol.Write_Message (Out_Buf);
elsif Is_List then
Hermes_Protocol.Make_Tools_List_Response (Id, Out_Buf);
Hermes_Protocol.Write_Message (Out_Buf);
elsif Is_Call then
declare
Input_Txt : Bounded_Text;
Uid_Txt : Bounded_Text;
Chan_Txt : Bounded_Text;
Srv_Txt : Bounded_Text;
Key : Bounded_Text;
Result : Bounded_Text;
Cyc_St : Operation_Status;
begin
Hermes_Protocol.Extract_Field (In_Buf, "input", Input_Txt);
Hermes_Protocol.Extract_Field (In_Buf, "uid", Uid_Txt);
Hermes_Protocol.Extract_Field (In_Buf, "channel", Chan_Txt);
Hermes_Protocol.Extract_Field (In_Buf, "server", Srv_Txt);
if Input_Txt.Length = 0 then
Hermes_Protocol.Make_Error_Response
(Id, -32602, "missing 'input' argument", Out_Buf);
else
Key := Soul.State.Make_Session_Key
(To_String (Uid_Txt),
To_String (Chan_Txt),
To_String (Srv_Txt));
Ada_Medium.Run_Inference_Cycle
(Key, Input_Txt, Result, Cyc_St);
if Cyc_St = OK then
Hermes_Protocol.Make_Tool_Result_Response
(Id, Result, Out_Buf);
else
Hermes_Protocol.Make_Error_Response
(Id, -32000, "inference cycle failed", Out_Buf);
end if;
end if;
Hermes_Protocol.Write_Message (Out_Buf);
end;
elsif Is_Notif then
null; -- notifications take no response
else
Hermes_Protocol.Make_Error_Response
(Id, -32601, "method not found", Out_Buf);
Hermes_Protocol.Write_Message (Out_Buf);
end if;
end if;
end;
end loop;
end Mafiabot;
mafiabot_core/src/organs/ada_medium/ada_medium.adb
+341
View File
@@ -0,0 +1,341 @@
with Soul.State;
package body Ada_Medium
with SPARK_Mode => On
is
-- Internal toolkit state
Toolkit : ML_Toolkit :=
(LoRA_Adapter => (Tool => LoRA_Adapter, Enabled => False),
SAE_Steering => (Tool => SAE_Steering, Enabled => False),
BERT_Classifier => (Tool => BERT_Classifier, Enabled => False),
RAG_Retrieval => (Tool => RAG_Retrieval, Enabled => False));
-- -----------------------------------------------------------------------
-- Phase transition table: only forward steps are legal.
-- Phase_Input is the universal reset target.
function Next_Legal (Current : Inference_Phase) return Inference_Phase is
begin
if Current = Phase_Coherence then
return Phase_Input; -- wrap after full cycle
else
return Inference_Phase'Succ (Current);
end if;
end Next_Legal;
-- -----------------------------------------------------------------------
protected body Inference_Orchestrator is
procedure Advance
(Next : in Inference_Phase;
Status : out Operation_Status)
is
begin
if Next = Next_Legal (Current) then
Current := Next;
Status := OK;
else
-- Illegal jump: reset to Phase_Input
Current := Phase_Input;
Status := Error_Invalid_State;
end if;
end Advance;
function Get_Current return Inference_Phase is (Current);
procedure Reset is
begin
Current := Phase_Input;
end Reset;
end Inference_Orchestrator;
-- -----------------------------------------------------------------------
procedure Route_Message
(Msg : in Organ_Message;
Status : out Operation_Status)
is
begin
Trust_Boundary.Trust_Guard.Screen_Inbound (Msg, Status);
end Route_Message;
-- -----------------------------------------------------------------------
-- Helpers that build organ messages for each cycle step
function Make_Internal_Msg
(Src : Organ_Id;
Dst : Organ_Id;
Text : Bounded_Text) return Organ_Message
is
begin
return (Source => Src,
Destination => Dst,
Provenance => System_Internal,
Payload => Text);
end Make_Internal_Msg;
-- Build a metacognitive prompt envelope for a Western phase.
function WMC_Envelope
(Phase : Natural;
Input : Bounded_Text) return Bounded_Text
is
Labels : constant array (1 .. 4) of String (1 .. 32) :=
("WMC1:SOCRATIC_APORIA ",
"WMC2:KANTIAN_BOUNDARIES ",
"WMC3:FREUD_HEGEL_DEPTH ",
"WMC4:MODERN_PRAGMATIC ");
Label_Len : constant := 24;
Pfx : constant String := "[";
Sep : constant String := "]";
L : constant String := Labels (Phase) (1 .. Label_Len);
Env : Bounded_Text;
Len : constant Natural := Pfx'Length + L'Length + Sep'Length + Input.Length;
begin
if Len <= Max_Text_Length then
Env.Length := Len;
declare
P : Natural := 1;
begin
Env.Data (P .. P + Pfx'Length - 1) := Pfx; P := P + Pfx'Length;
Env.Data (P .. P + L'Length - 1) := L; P := P + L'Length;
Env.Data (P .. P + Sep'Length - 1) := Sep; P := P + Sep'Length;
Env.Data (P .. P + Input.Length - 1) :=
Input.Data (1 .. Input.Length);
end;
end if;
return Env;
end WMC_Envelope;
-- Build a metacognitive prompt envelope for a Non-Western phase.
function EMC_Envelope
(Phase : Natural;
Input : Bounded_Text) return Bounded_Text
is
Labels : constant array (1 .. 4) of String (1 .. 32) :=
("EMC1:IRANIAN_ASHA_DAENA ",
"EMC2:EAST_ASIAN_XIN_ZHAI ",
"EMC3:INDIC_SAKSHIBHAVA ",
"EMC4:TIBETAN_BON ");
Label_Len : constant := 24;
Pfx : constant String := "{";
Sep : constant String := "}";
L : constant String := Labels (Phase) (1 .. Label_Len);
Env : Bounded_Text;
Len : constant Natural := Pfx'Length + L'Length + Sep'Length + Input.Length;
begin
if Len <= Max_Text_Length then
Env.Length := Len;
declare
P : Natural := 1;
begin
Env.Data (P .. P + Pfx'Length - 1) := Pfx; P := P + Pfx'Length;
Env.Data (P .. P + L'Length - 1) := L; P := P + L'Length;
Env.Data (P .. P + Sep'Length - 1) := Sep; P := P + Sep'Length;
Env.Data (P .. P + Input.Length - 1) :=
Input.Data (1 .. Input.Length);
end;
end if;
return Env;
end EMC_Envelope;
-- Append Suffix to Accumulator (truncate silently if overflow)
procedure Accumulate
(Accum : in out Bounded_Text;
Suffix : in Bounded_Text)
is
Available : constant Natural := Max_Text_Length - Accum.Length;
To_Copy : constant Natural :=
(if Suffix.Length <= Available then Suffix.Length else Available);
begin
Accum.Data (Accum.Length + 1 .. Accum.Length + To_Copy) :=
Suffix.Data (1 .. To_Copy);
Accum.Length := Accum.Length + To_Copy;
end Accumulate;
-- -----------------------------------------------------------------------
procedure Run_Inference_Cycle
(Session_Key : in Bounded_Text;
Input : in Bounded_Text;
Output : out Bounded_Text;
Status : out Operation_Status)
is
S : Operation_Status;
Accum : Bounded_Text; -- accumulates enriched context across all steps
Msg : Organ_Message;
Ref : Soul.State.Session_Ref := Soul.State.No_Session;
begin
Output := (others => ' ', Length => 0);
Inference_Orchestrator.Reset;
-- Resolve the session for this (uid, channel, server). The cross and
-- card pool below belong to THIS session only.
Soul.State.Soul_State.Open_Session (Session_Key, Ref, S);
if S /= OK then Status := S; return; end if;
if Ref not in Soul.State.Valid_Session then
Status := Error_Invalid_State;
return;
end if;
-- Step 1: INPUT. Reset already leaves the orchestrator AT Phase_Input,
-- so this step does its work directly rather than advancing onto itself.
Accumulate (Accum, Input);
-- Step 2: Ada enriches
Inference_Orchestrator.Advance (Phase_Enrich, S);
if S /= OK then Status := S; return; end if;
-- (Drive-Box enrichment deferred to follow-up session;
-- RAG context would be injected here when implemented.)
-- Step 3: LLM init
Inference_Orchestrator.Advance (Phase_LLM_Init, S);
if S /= OK then Status := S; return; end if;
-- The Celtic Cross is NOT drawn whole here. It accretes through the
-- cognitive loops below — 2 cards per layer (steps 6/9/13), the stave
-- of 4 last (step 17). Once formed it is held for the whole session
-- (or 17 outputs, whichever is longer); Soul_State owns that state, so
-- later cycles in the session reuse the same cross instead of redrawing.
-- Steps 4–5: wMC1 + eMC1
Inference_Orchestrator.Advance (Phase_WMC1, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, WMC_Envelope (1, Accum));
Inference_Orchestrator.Advance (Phase_EMC1, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, EMC_Envelope (1, Accum));
-- Step 6: CC layer 1 (Present, Challenge) accretes from the loop
Inference_Orchestrator.Advance (Phase_CC_1_2, S);
if S /= OK then Status := S; return; end if;
if not Soul.State.Soul_State.Is_Spread_Formed (Ref) then
Soul.State.Soul_State.Form_Layer (Ref, Soul.Celtic_Cross.Layer_1, S);
if S /= OK then Status := S; return; end if;
end if;
Accumulate
(Accum,
Soul.Celtic_Cross.Step_6_Context
(Soul.State.Soul_State.Current_Spread (Ref)));
-- Steps 7–8: wMC2 + eMC2
Inference_Orchestrator.Advance (Phase_WMC2, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, WMC_Envelope (2, Accum));
Inference_Orchestrator.Advance (Phase_EMC2, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, EMC_Envelope (2, Accum));
-- Step 9: CC layer 2 (Foundation, Recent_Past) accretes from the loop
Inference_Orchestrator.Advance (Phase_CC_3_4, S);
if S /= OK then Status := S; return; end if;
if not Soul.State.Soul_State.Is_Spread_Formed (Ref) then
Soul.State.Soul_State.Form_Layer (Ref, Soul.Celtic_Cross.Layer_2, S);
if S /= OK then Status := S; return; end if;
end if;
Accumulate
(Accum,
Soul.Celtic_Cross.Step_9_Context
(Soul.State.Soul_State.Current_Spread (Ref)));
-- Step 10: llmCog 1
Inference_Orchestrator.Advance (Phase_LLM_Cog_1, S);
if S /= OK then Status := S; return; end if;
-- (LLM call issued via protocol layer in full implementation)
-- Steps 11–12: wMC3 + eMC3
Inference_Orchestrator.Advance (Phase_WMC3, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, WMC_Envelope (3, Accum));
Inference_Orchestrator.Advance (Phase_EMC3, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, EMC_Envelope (3, Accum));
-- Step 13: CC layer 3 (Crown, Near_Future) accretes from the loop
Inference_Orchestrator.Advance (Phase_CC_5_6, S);
if S /= OK then Status := S; return; end if;
if not Soul.State.Soul_State.Is_Spread_Formed (Ref) then
Soul.State.Soul_State.Form_Layer (Ref, Soul.Celtic_Cross.Layer_3, S);
if S /= OK then Status := S; return; end if;
end if;
Accumulate
(Accum,
Soul.Celtic_Cross.Step_13_Context
(Soul.State.Soul_State.Current_Spread (Ref)));
-- Step 14: llmCog 2
Inference_Orchestrator.Advance (Phase_LLM_Cog_2, S);
if S /= OK then Status := S; return; end if;
-- Steps 15–16: wMC4 + eMC4
Inference_Orchestrator.Advance (Phase_WMC4, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, WMC_Envelope (4, Accum));
Inference_Orchestrator.Advance (Phase_EMC4, S);
if S /= OK then Status := S; return; end if;
Accumulate (Accum, EMC_Envelope (4, Accum));
-- Step 17: CC stave (Self_Attitude .. Outcome) pulled as a block once
-- the 4x4 cognition completes — this is what finishes the cross.
Inference_Orchestrator.Advance (Phase_CC_7_10, S);
if S /= OK then Status := S; return; end if;
if not Soul.State.Soul_State.Is_Spread_Formed (Ref) then
Soul.State.Soul_State.Form_Layer (Ref, Soul.Celtic_Cross.Stave, S);
if S /= OK then Status := S; return; end if;
end if;
Accumulate
(Accum,
Soul.Celtic_Cross.Step_17_Context
(Soul.State.Soul_State.Current_Spread (Ref)));
-- Step 18: finalLLMcog
Inference_Orchestrator.Advance (Phase_Final_Cog, S);
if S /= OK then Status := S; return; end if;
-- Step 19: mini-rag (schema lookup — stub until mini-rag organ added)
Inference_Orchestrator.Advance (Phase_Mini_Rag, S);
if S /= OK then Status := S; return; end if;
-- Step 20: sendAda
Inference_Orchestrator.Advance (Phase_Send_Ada, S);
if S /= OK then Status := S; return; end if;
Msg := Make_Internal_Msg (Ada_Medium, Ada_Medium, Accum);
-- Step 21: Ada routes (trust boundary outbound screen)
Inference_Orchestrator.Advance (Phase_Route, S);
if S /= OK then Status := S; return; end if;
Trust_Boundary.Trust_Guard.Screen_Outbound (Msg, S);
if S /= OK then Status := S; return; end if;
-- Step 22: Synthesize
Inference_Orchestrator.Advance (Phase_Synthesize, S);
if S /= OK then Status := S; return; end if;
-- Step 23: Coherence check (intent vs finalLLMcog drift detection)
Inference_Orchestrator.Advance (Phase_Coherence, S);
if S /= OK then Status := S; return; end if;
-- Record the completed output for this session. The session cross is now
-- held; it will not re-form until Soul_State.Reset_Spread (new session /
-- floor rollover).
Soul.State.Soul_State.Note_Output (Ref);
Output := Accum;
Status := OK;
end Run_Inference_Cycle;
-- -----------------------------------------------------------------------
function Active_Toolkit return ML_Toolkit is (Toolkit);
procedure Configure_Tool (Tool : ML_Tool; Enabled : Boolean) is
begin
Toolkit (Tool) := (Tool => Tool, Enabled => Enabled);
end Configure_Tool;
end Ada_Medium;
mafiabot_core/src/organs/ada_medium/ada_medium.ads
+110
View File
@@ -0,0 +1,110 @@
-- Ada Connective Medium — the organ-systems body's shared medium.
-- NOT a controller; organs are perfused BY it, not subordinated TO it.
--
-- Defines:
-- - Organ_Message (inter-organ communication)
-- - Inference_Phase enum (23-step cycle)
-- - Inference_Orchestrator protected object
-- - Run_Inference_Cycle — the top-level 23-step pipeline
with Mafiabot_Types; use Mafiabot_Types;
with Trust_Boundary;
with Soul.Celtic_Cross;
with System;
package Ada_Medium
with SPARK_Mode => On
is
-- Re-export Organ_Message from Trust_Boundary for callers
subtype Organ_Message is Trust_Boundary.Organ_Message;
-- ML toolchain interface descriptors (capability flags, not live handles)
type ML_Tool is (LoRA_Adapter, SAE_Steering, BERT_Classifier, RAG_Retrieval);
type Tool_Descriptor is record
Tool : ML_Tool;
Enabled : Boolean := False;
end record;
type ML_Toolkit is array (ML_Tool) of Tool_Descriptor;
-- -----------------------------------------------------------------------
-- Inference cycle: 23 steps
type Inference_Phase is (
Phase_Input, -- 1 INPUT received
Phase_Enrich, -- 2 Ada enriches (drive state + RAG context)
Phase_LLM_Init, -- 3 LLM init.thoughtChain
Phase_WMC1, -- 4 wMC1 Socratic destabilisation
Phase_EMC1, -- 5 eMC1 Iranian Asha/Daena alignment
Phase_CC_1_2, -- 6 CC cards 1 & 2 injected
Phase_WMC2, -- 7 wMC2 Kantian boundary mapping
Phase_EMC2, -- 8 eMC2 East Asian Xin-Zhai mirror
Phase_CC_3_4, -- 9 CC cards 3 & 4 injected
Phase_LLM_Cog_1, -- 10 first llmCog
Phase_WMC3, -- 11 wMC3 Freud/Hegel depth
Phase_EMC3, -- 12 eMC3 Indic Sakshibhava witness
Phase_CC_5_6, -- 13 CC cards 5 & 6 injected
Phase_LLM_Cog_2, -- 14 second llmCog
Phase_WMC4, -- 15 wMC4 modern pragmatic stream
Phase_EMC4, -- 16 eMC4 Tibetan Bön elemental flow
Phase_CC_7_10, -- 17 CC cards 7–10 injected
Phase_Final_Cog, -- 18 finalLLMcog
Phase_Mini_Rag, -- 19 mini-rag JIT schema lookup
Phase_Send_Ada, -- 20 sendAda
Phase_Route, -- 21 Ada routes to tools
Phase_Synthesize, -- 22 Synthesize
Phase_Coherence -- 23 Coherence check / drift detection
);
-- -----------------------------------------------------------------------
-- Inference orchestrator — enforces forward-only phase progression.
-- Illegal jumps yield Error_Invalid_State and halt the cycle.
protected Inference_Orchestrator is
pragma Priority (System.Priority'Last);
procedure Advance
(Next : in Inference_Phase;
Status : out Operation_Status)
with Post =>
(if Status = OK then
Get_Current = Next
else
Get_Current = Phase_Input); -- reset on illegal jump
function Get_Current return Inference_Phase;
procedure Reset;
private
Current : Inference_Phase := Phase_Input;
end Inference_Orchestrator;
-- -----------------------------------------------------------------------
-- Message routing through the trust boundary
procedure Route_Message
(Msg : in Organ_Message;
Status : out Operation_Status)
with Pre => Msg.Payload.Length > 0;
-- -----------------------------------------------------------------------
-- Top-level 23-step inference cycle.
--
-- Session_Key scopes the Celtic Cross and card pool to one (uid, channel,
-- server) tuple — compose it with Soul.State.Make_Session_Key. Distinct
-- sessions never share a deck or a cross; the Big-3 identity is global.
procedure Run_Inference_Cycle
(Session_Key : in Bounded_Text;
Input : in Bounded_Text;
Output : out Bounded_Text;
Status : out Operation_Status)
with Pre => Input.Length > 0;
-- Toolkit accessor (configured at startup)
function Active_Toolkit return ML_Toolkit;
procedure Configure_Tool (Tool : ML_Tool; Enabled : Boolean);
end Ada_Medium;
mafiabot_core/src/organs/soul/soul-celtic_cross.adb
+278
View File
@@ -0,0 +1,278 @@
package body Soul.Celtic_Cross
with SPARK_Mode => On
is
procedure Draw_Spread
(D : in out Soul.Tarot.Deck;
Spread : out CC_Spread;
Status : out Operation_Status)
is
Drawn : Natural := 0;
Pos : CC_Position := CC_Position'First;
begin
Spread := (others => (State => Soul.Tarot.Absent,
Value => (Kind => Soul.Tarot.Major,
Major_Value => Soul.Tarot.The_Fool)));
if Soul.Tarot.Present_Count (D) < 10 then
Status := Error_Deck_Empty;
return;
end if;
for I in Soul.Tarot.Deck_Index loop
exit when Drawn = 10;
if D (I).State = Soul.Tarot.Present then
Spread (Pos) := D (I);
D (I).State := Soul.Tarot.Absent;
Drawn := Drawn + 1;
if Pos /= CC_Position'Last then
Pos := CC_Position'Succ (Pos);
end if;
end if;
end loop;
Status := OK;
end Draw_Spread;
-- ------------------------------------------------------------------
function Empty_Spread return CC_Spread is
begin
return (others => (State => Soul.Tarot.Absent,
Value => (Kind => Soul.Tarot.Major,
Major_Value => Soul.Tarot.The_Fool)));
end Empty_Spread;
procedure Draw_Layer
(D : in out Soul.Tarot.Deck;
Spread : in out CC_Spread;
Layer : in CC_Layer;
Status : out Operation_Status)
is
Need : constant Positive := Cards_In_Layer (Layer);
Targets : array (1 .. 4) of CC_Position := (others => CC_Position'First);
Count : Natural := 0;
begin
case Layer is
when Layer_1 =>
Targets (1) := Present; Targets (2) := Challenge;
when Layer_2 =>
Targets (1) := Foundation; Targets (2) := Recent_Past;
when Layer_3 =>
Targets (1) := Crown; Targets (2) := Near_Future;
when Stave =>
Targets (1) := Self_Attitude; Targets (2) := Environment;
Targets (3) := Hopes_Fears; Targets (4) := Outcome;
end case;
if Soul.Tarot.Present_Count (D) < Need then
Status := Error_Deck_Empty;
return;
end if;
for I in Soul.Tarot.Deck_Index loop
exit when Count = Need;
if D (I).State = Soul.Tarot.Present then
Spread (Targets (Count + 1)) := D (I);
D (I).State := Soul.Tarot.Absent;
Count := Count + 1;
end if;
end loop;
Status := OK;
end Draw_Layer;
-- ------------------------------------------------------------------
-- Card token serialisation
function Major_Token (M : Soul.Tarot.Major_Arcana) return String is
begin
case M is
when Soul.Tarot.The_Fool => return "THE_FOOL";
when Soul.Tarot.The_Magician => return "THE_MAGICIAN";
when Soul.Tarot.The_High_Priestess => return "HIGH_PRIESTESS";
when Soul.Tarot.The_Empress => return "THE_EMPRESS";
when Soul.Tarot.The_Emperor => return "THE_EMPEROR";
when Soul.Tarot.The_Hierophant => return "THE_HIEROPHANT";
when Soul.Tarot.The_Lovers => return "THE_LOVERS";
when Soul.Tarot.The_Chariot => return "THE_CHARIOT";
when Soul.Tarot.Adjustment => return "ADJUSTMENT";
when Soul.Tarot.The_Hermit => return "THE_HERMIT";
when Soul.Tarot.Fortune => return "FORTUNE";
when Soul.Tarot.Lust => return "LUST";
when Soul.Tarot.The_Hanged_Man => return "THE_HANGED_MAN";
when Soul.Tarot.Death => return "DEATH";
when Soul.Tarot.Art => return "ART";
when Soul.Tarot.The_Devil => return "THE_DEVIL";
when Soul.Tarot.The_Tower => return "THE_TOWER";
when Soul.Tarot.The_Star => return "THE_STAR";
when Soul.Tarot.The_Moon => return "THE_MOON";
when Soul.Tarot.The_Sun => return "THE_SUN";
when Soul.Tarot.The_Aeon => return "THE_AEON";
when Soul.Tarot.The_Universe => return "THE_UNIVERSE";
when Soul.Tarot.SD_Maya => return "SD_MAYA";
when Soul.Tarot.SD_History => return "SD_HISTORY";
when Soul.Tarot.SD_Virus => return "SD_VIRUS";
when Soul.Tarot.SD_Achievement => return "SD_ACHIEVEMENT";
when Soul.Tarot.SD_Digital => return "SD_DIGITAL";
when Soul.Tarot.SD_Vulture_Mother => return "SD_VULTURE_MOTHER";
when Soul.Tarot.SD_She_Is_Legend => return "SD_SHE_IS_LEGEND";
when Soul.Tarot.SD_Schrodinger => return "SD_SCHRODINGER";
when Soul.Tarot.SD_Singularity => return "SD_SINGULARITY";
end case;
end Major_Token;
function Suit_Token (S : Soul.Tarot.Suit) return String is
begin
case S is
when Soul.Tarot.Wands => return "WANDS";
when Soul.Tarot.Cups => return "CUPS";
when Soul.Tarot.Swords => return "SWORDS";
when Soul.Tarot.Pentacles => return "PENTACLES";
end case;
end Suit_Token;
function Rank_Token (R : Soul.Tarot.Court_Rank) return String is
begin
case R is
when Soul.Tarot.Ninety_Nine => return "99";
when Soul.Tarot.King => return "KING";
when Soul.Tarot.Queen => return "QUEEN";
when Soul.Tarot.Chevalier => return "CHEVALIER";
when Soul.Tarot.P => return "P";
end case;
end Rank_Token;
function Void_Token (V : Soul.Tarot.Void_Card) return String is
begin
case V is
when Soul.Tarot.Void_Queen => return "VOID_QUEEN";
when Soul.Tarot.Void_King => return "VOID_KING";
when Soul.Tarot.Void_Chevalier => return "VOID_CHEVALIER";
when Soul.Tarot.Void_Progeny => return "VOID_PROGENY";
when Soul.Tarot.Void_Zero => return "VOID_ZERO";
end case;
end Void_Token;
function Card_Token (C : Soul.Tarot.Card) return Bounded_Text is
S : String (1 .. 64) := (others => ' ');
L : Natural := 0;
begin
case C.Kind is
when Soul.Tarot.Major =>
declare
T : constant String := Major_Token (C.Major_Value);
begin
L := T'Length;
S (1 .. L) := T;
end;
when Soul.Tarot.Court =>
declare
R : constant String := Rank_Token (C.Rank_Value);
U : constant String := Suit_Token (C.Suit_Value);
Combined : constant String := R & "_OF_" & U;
begin
L := Combined'Length;
if L <= 64 then
S (1 .. L) := Combined;
end if;
end;
when Soul.Tarot.Void_Suit =>
declare
T : constant String := Void_Token (C.Void_Value);
begin
L := T'Length;
S (1 .. L) := T;
end;
end case;
declare
Result : Bounded_Text;
begin
if L <= Max_Text_Length then
Result.Length := L;
Result.Data (1 .. L) := S (1 .. L);
end if;
return Result;
end;
end Card_Token;
-- Build a two-card context string "[POS: TOKEN, POS: TOKEN]"
function Two_Card_Context
(P1 : CC_Position; C1 : Soul.Tarot.Deck_Slot;
P2 : CC_Position; C2 : Soul.Tarot.Deck_Slot) return Bounded_Text
is
pragma Unreferenced (P1, P2);
T1 : constant Bounded_Text :=
(if C1.State = Soul.Tarot.Present then Card_Token (C1.Value)
else Make_Text ("ABSENT"));
T2 : constant Bounded_Text :=
(if C2.State = Soul.Tarot.Present then Card_Token (C2.Value)
else Make_Text ("ABSENT"));
Prefix : constant String := "[CC:";
Sep : constant String := "|";
Suffix : constant String := "]";
Combined_Len : constant Natural :=
Prefix'Length + T1.Length + Sep'Length + T2.Length + Suffix'Length;
Result : Bounded_Text;
begin
if Combined_Len <= Max_Text_Length then
Result.Length := Combined_Len;
declare
P : Natural := 1;
begin
Result.Data (P .. P + Prefix'Length - 1) := Prefix;
P := P + Prefix'Length;
Result.Data (P .. P + T1.Length - 1) := T1.Data (1 .. T1.Length);
P := P + T1.Length;
Result.Data (P .. P + Sep'Length - 1) := Sep;
P := P + Sep'Length;
Result.Data (P .. P + T2.Length - 1) := T2.Data (1 .. T2.Length);
P := P + T2.Length;
Result.Data (P .. P + Suffix'Length - 1) := Suffix;
end;
end if;
return Result;
end Two_Card_Context;
function Step_6_Context (S : CC_Spread) return Bounded_Text is
begin
return Two_Card_Context (Present, S (Present),
Challenge, S (Challenge));
end Step_6_Context;
function Step_9_Context (S : CC_Spread) return Bounded_Text is
begin
return Two_Card_Context (Foundation, S (Foundation),
Recent_Past, S (Recent_Past));
end Step_9_Context;
function Step_13_Context (S : CC_Spread) return Bounded_Text is
begin
return Two_Card_Context (Crown, S (Crown),
Near_Future, S (Near_Future));
end Step_13_Context;
function Step_17_Context (S : CC_Spread) return Bounded_Text is
-- Four cards — build as two concatenated two-card strings
First : constant Bounded_Text :=
Two_Card_Context (Self_Attitude, S (Self_Attitude),
Environment, S (Environment));
Second : constant Bounded_Text :=
Two_Card_Context (Hopes_Fears, S (Hopes_Fears),
Outcome, S (Outcome));
Sep : constant String := ";";
Combined_Len : constant Natural :=
First.Length + Sep'Length + Second.Length;
Result : Bounded_Text;
begin
if Combined_Len <= Max_Text_Length then
Result.Length := Combined_Len;
Result.Data (1 .. First.Length) := First.Data (1 .. First.Length);
Result.Data (First.Length + 1 .. First.Length + Sep'Length) := Sep;
Result.Data (First.Length + Sep'Length + 1 .. Combined_Len) :=
Second.Data (1 .. Second.Length);
end if;
return Result;
end Step_17_Context;
end Soul.Celtic_Cross;
mafiabot_core/src/organs/soul/soul-celtic_cross.ads
+84
View File
@@ -0,0 +1,84 @@
-- Celtic Cross spread — 10-position layout mapped to inference cycle steps.
--
-- Position → Inference step:
-- Present, Challenge → Step 6 (CC_Cards_1_2)
-- Foundation, Recent_Past → Step 9 (CC_Cards_3_4)
-- Crown, Near_Future → Step 13 (CC_Cards_5_6)
-- Self_Attitude..Outcome (4 cards) → Step 17 (CC_Cards_7_10)
--
-- Cards apply iteratively: each draw stays in the accumulation context for
-- all subsequent llmCog passes in the same inference cycle.
with Soul.Tarot;
with Mafiabot_Types; use Mafiabot_Types;
package Soul.Celtic_Cross
with SPARK_Mode => On
is
type CC_Position is (
Present,
Challenge,
Foundation,
Recent_Past,
Crown,
Near_Future,
Self_Attitude,
Environment,
Hopes_Fears,
Outcome
);
type CC_Spread is array (CC_Position) of Soul.Tarot.Deck_Slot;
-- An empty (all-Absent) spread — the starting point before the cross
-- accretes through the cognitive loops.
function Empty_Spread return CC_Spread;
-- The cross does not arrive whole. It accretes 2 cards per cognitive
-- layer across the 4x4 metacognitive multicycle, then the stave (the
-- 4-card staff) is pulled as a block once the loops complete:
-- Layer_1 (after wMC1/eMC1, step 6) -> Present, Challenge
-- Layer_2 (after wMC2/eMC2, step 9) -> Foundation, Recent_Past
-- Layer_3 (after wMC3/eMC3, step 13) -> Crown, Near_Future
-- Stave (after wMC4/eMC4, step 17) -> Self_Attitude .. Outcome
type CC_Layer is (Layer_1, Layer_2, Layer_3, Stave);
-- Number of card positions a given layer fills.
function Cards_In_Layer (L : CC_Layer) return Positive is
(if L = Stave then 4 else 2);
-- Draw one layer's cards from the dynamic deck into the spread.
-- Cards already present in the spread are left untouched. Removes the
-- drawn cards from D. Returns Error_Deck_Empty if the deck cannot
-- supply the layer.
procedure Draw_Layer
(D : in out Soul.Tarot.Deck;
Spread : in out CC_Spread;
Layer : in CC_Layer;
Status : out Operation_Status)
with Post => (if Status = OK then
Soul.Tarot.Present_Count (D) =
Soul.Tarot.Present_Count (D'Old) - Cards_In_Layer (Layer));
-- Draw all ten cards at once from the dynamic deck (removes them from D).
-- Convenience wrapper used by tests; the live cycle uses Draw_Layer.
-- If fewer than 10 cards are present, returns Error_Deck_Empty.
procedure Draw_Spread
(D : in out Soul.Tarot.Deck;
Spread : out CC_Spread;
Status : out Operation_Status)
with Post => (if Status = OK then
Soul.Tarot.Present_Count (D) =
Soul.Tarot.Present_Count (D'Old) - 10);
-- Card names as short Bounded_Text tokens for prompt injection.
function Card_Token (C : Soul.Tarot.Card) return Bounded_Text;
-- Serialise the spread slice for a given step into a Bounded_Text
-- that can be injected into the metacognitive context.
function Step_6_Context (S : CC_Spread) return Bounded_Text;
function Step_9_Context (S : CC_Spread) return Bounded_Text;
function Step_13_Context (S : CC_Spread) return Bounded_Text;
function Step_17_Context (S : CC_Spread) return Bounded_Text;
end Soul.Celtic_Cross;
mafiabot_core/src/organs/soul/soul-state.adb
+221
View File
@@ -0,0 +1,221 @@
package body Soul.State
with SPARK_Mode => On
is
function Make_Session_Key
(Uid : String;
Channel : String;
Server : String) return Bounded_Text
is
function D (S : String) return String is
(if S'Length = 0 then "default" else S);
Composed : constant String :=
D (Uid) & "|" & D (Channel) & "|" & D (Server);
begin
if Composed'Length <= Max_Text_Length then
return Make_Text (Composed);
else
return Make_Text
(Composed (Composed'First .. Composed'First + Max_Text_Length - 1));
end if;
end Make_Session_Key;
protected body Soul_State is
-- ---- internal helpers ------------------------------------------
function Keys_Equal (K : Session_Key; B : Bounded_Text) return Boolean is
Eff : constant Natural :=
(if B.Length <= Max_Key then B.Length else Max_Key);
begin
return K.Length = Eff
and then K.Data (1 .. Eff) = B.Data (1 .. Eff);
end Keys_Equal;
procedure Set_Key (K : out Session_Key; B : Bounded_Text) is
Eff : constant Natural :=
(if B.Length <= Max_Key then B.Length else Max_Key);
begin
K.Data := (others => ' ');
K.Length := Eff;
if Eff > 0 then
K.Data (1 .. Eff) := B.Data (1 .. Eff);
end if;
end Set_Key;
-- ---- identity --------------------------------------------------
procedure Initialize_Big_Three
(B3 : in Soul.Tarot.Big_Three;
Status : out Operation_Status)
is
begin
if Initialized then
Status := Error_Already_Init;
return;
end if;
if not Soul.Tarot.Big_Three_Distinct (B3) then
Status := Error_Config;
return;
end if;
Big_3 := B3;
Initialized := True;
Status := OK;
end Initialize_Big_Three;
-- ---- sessions --------------------------------------------------
procedure Open_Session
(Key : in Bounded_Text;
Ref : out Session_Ref;
Status : out Operation_Status)
is
Free : Session_Ref := No_Session;
Remove_Status : Operation_Status;
begin
Ref := No_Session;
for I in Valid_Session loop
if Sessions (I).In_Use then
if Keys_Equal (Sessions (I).Key, Key) then
Ref := I;
Status := OK;
return;
end if;
elsif Free = No_Session then
Free := I;
end if;
end loop;
if Free = No_Session then
Status := Error_Overflow;
return;
end if;
-- Allocate a fresh session: full deck minus the immutable Big-3.
Set_Key (Sessions (Free).Key, Key);
Sessions (Free).Deck := Soul.Tarot.Full_Deck;
Soul.Tarot.Remove_Big_Three
(Sessions (Free).Deck, Big_3, Remove_Status);
if Remove_Status /= OK then
Status := Remove_Status;
return; -- slot left free (In_Use still False)
end if;
Sessions (Free).Spread := Soul.Celtic_Cross.Empty_Spread;
Sessions (Free).Layer_Done := (others => False);
Sessions (Free).Output_Counter := 0;
Sessions (Free).In_Use := True;
Ref := Free;
Status := OK;
end Open_Session;
procedure Form_Layer
(Ref : in Valid_Session;
Layer : in Soul.Celtic_Cross.CC_Layer;
Status : out Operation_Status)
is
begin
-- Idempotent: a layer already drawn this session is held, not redrawn.
if Sessions (Ref).Layer_Done (Layer) then
Status := OK;
return;
end if;
Soul.Celtic_Cross.Draw_Layer
(Sessions (Ref).Deck, Sessions (Ref).Spread, Layer, Status);
if Status = OK then
Sessions (Ref).Layer_Done (Layer) := True;
end if;
end Form_Layer;
procedure Reset_Spread (Ref : in Valid_Session) is
begin
Sessions (Ref).Spread := Soul.Celtic_Cross.Empty_Spread;
Sessions (Ref).Layer_Done := (others => False);
end Reset_Spread;
procedure Note_Output (Ref : in Valid_Session) is
begin
if Sessions (Ref).Output_Counter < Natural'Last then
Sessions (Ref).Output_Counter := Sessions (Ref).Output_Counter + 1;
end if;
end Note_Output;
-- ---- SOUL.md ---------------------------------------------------
procedure Generate_Soul_MD
(Buffer : out Bounded_Text;
Status : out Operation_Status)
is
Sun_T : constant Bounded_Text :=
Soul.Celtic_Cross.Card_Token (Big_3.Sun);
Moon_T : constant Bounded_Text :=
Soul.Celtic_Cross.Card_Token (Big_3.Moon);
Asc_T : constant Bounded_Text :=
Soul.Celtic_Cross.Card_Token (Big_3.Ascendant);
Header : constant String := "# SOUL" & ASCII.LF;
Sun_L : constant String := "## Sun: ";
Moon_L : constant String := ASCII.LF & "## Moon: ";
Asc_L : constant String := ASCII.LF & "## Ascendant: ";
Footer : constant String := ASCII.LF;
Total : constant Natural :=
Header'Length
+ Sun_L'Length + Sun_T.Length
+ Moon_L'Length + Moon_T.Length
+ Asc_L'Length + Asc_T.Length
+ Footer'Length;
begin
Buffer := (others => ' ', Length => 0);
if Total > Max_Text_Length then
Status := Error_Overflow;
return;
end if;
declare
P : Natural := 1;
begin
Buffer.Data (P .. P + Header'Length - 1) := Header; P := P + Header'Length;
Buffer.Data (P .. P + Sun_L'Length - 1) := Sun_L; P := P + Sun_L'Length;
Buffer.Data (P .. P + Sun_T.Length - 1) := Sun_T.Data (1 .. Sun_T.Length);
P := P + Sun_T.Length;
Buffer.Data (P .. P + Moon_L'Length - 1) := Moon_L; P := P + Moon_L'Length;
Buffer.Data (P .. P + Moon_T.Length - 1) := Moon_T.Data (1 .. Moon_T.Length);
P := P + Moon_T.Length;
Buffer.Data (P .. P + Asc_L'Length - 1) := Asc_L; P := P + Asc_L'Length;
Buffer.Data (P .. P + Asc_T.Length - 1) := Asc_T.Data (1 .. Asc_T.Length);
P := P + Asc_T.Length;
Buffer.Data (P .. P + Footer'Length - 1) := Footer;
end;
Buffer.Length := Total;
Status := OK;
end Generate_Soul_MD;
-- ---- accessors -------------------------------------------------
function Is_Initialized return Boolean is (Initialized);
function Get_Big_Three return Soul.Tarot.Big_Three is (Big_3);
function Is_Spread_Formed (Ref : Valid_Session) return Boolean is
(for all L in Soul.Celtic_Cross.CC_Layer => Sessions (Ref).Layer_Done (L));
function Current_Spread (Ref : Valid_Session)
return Soul.Celtic_Cross.CC_Spread is (Sessions (Ref).Spread);
function Output_Count (Ref : Valid_Session) return Natural is
(Sessions (Ref).Output_Counter);
function Session_Count return Natural is
N : Natural := 0;
begin
for I in Valid_Session loop
if Sessions (I).In_Use then
N := N + 1;
end if;
end loop;
return N;
end Session_Count;
end Soul_State;
end Soul.State;
mafiabot_core/src/organs/soul/soul-state.ads
+125
View File
@@ -0,0 +1,125 @@
-- Soul_State protected object.
--
-- Holds two kinds of state:
-- * Global identity — the Big-3 (Sun/Moon/Ascendant). This is WHO Ada is,
-- immutable once set, shared across every conversation.
-- * Per-session context — each (uid, channel, server) tuple gets its own
-- dynamic card pool, Celtic Cross spread, and output counter. The cross
-- forms from that session's cognitive loops and is held for the session
-- (or Spread_Output_Floor outputs, whichever is longer). Two users on two
-- channels never share a deck or a cross.
--
-- Generates SOUL.md content for the Hermes Agent identity slot.
with Soul.Tarot;
with Soul.Celtic_Cross;
with Mafiabot_Types; use Mafiabot_Types;
with System;
package Soul.State
with SPARK_Mode => On
is
-- Lifetime floor for a Celtic Cross spread. A formed cross is held for
-- the whole session OR this many outputs, whichever is longer. Within a
-- single running binary the session always wins (the cross is formed once
-- and held); the floor only governs carrying a spread across a restart,
-- which requires deck-state serialisation (deferred).
Spread_Output_Floor : constant := 17;
-- Maximum number of concurrent sessions (uid x channel x server tuples).
Max_Sessions : constant := 64;
-- Opaque session handle. 0 is the null handle (no session); 1 .. Max is a
-- live slot returned by Open_Session.
type Session_Ref is range 0 .. Max_Sessions;
No_Session : constant Session_Ref := 0;
subtype Valid_Session is Session_Ref range 1 .. Max_Sessions;
-- Compose a canonical session key from the routing identity. Any field may
-- be empty; missing fields default to "default" so a bare call still maps
-- to a stable session.
function Make_Session_Key
(Uid : String;
Channel : String;
Server : String) return Bounded_Text;
protected Soul_State is
pragma Priority (System.Priority'Last - 2);
-- Set the three immutable personality anchors. Fails if called twice.
procedure Initialize_Big_Three
(B3 : in Soul.Tarot.Big_Three;
Status : out Operation_Status)
with Post => (if Status = OK then Is_Initialized);
-- Resolve a session by key, allocating a fresh slot (with its own
-- Big-3-pruned deck) on first sight. Returns No_Session +
-- Error_Overflow if the table is full.
procedure Open_Session
(Key : in Bounded_Text;
Ref : out Session_Ref;
Status : out Operation_Status)
with Pre => Is_Initialized,
Post => (if Status = OK then Ref in Valid_Session);
-- Accrete one cognitive layer of THIS session's cross from its pool.
-- Idempotent per layer: re-forming an already-formed layer is a no-op
-- returning OK. The cross builds across the 4x4 multicycle (Layer_1/2/3
-- = 2 cards each, Stave = 4), then is held for the session.
procedure Form_Layer
(Ref : in Valid_Session;
Layer : in Soul.Celtic_Cross.CC_Layer;
Status : out Operation_Status);
-- Clear THIS session's cross so a fresh one forms (new session / floor
-- rollover). Does not touch Big-3 or refill the deck.
procedure Reset_Spread (Ref : in Valid_Session);
-- Record that one output (inference cycle) completed for THIS session.
procedure Note_Output (Ref : in Valid_Session);
-- Serialise the global identity into Bounded_Text for SOUL.md.
procedure Generate_Soul_MD
(Buffer : out Bounded_Text;
Status : out Operation_Status)
with Pre => Is_Initialized;
function Is_Initialized return Boolean;
function Get_Big_Three return Soul.Tarot.Big_Three;
function Is_Spread_Formed (Ref : Valid_Session) return Boolean;
function Current_Spread (Ref : Valid_Session)
return Soul.Celtic_Cross.CC_Spread;
function Output_Count (Ref : Valid_Session) return Natural;
function Session_Count return Natural;
private
Big_3 : Soul.Tarot.Big_Three;
Initialized : Boolean := False;
Max_Key : constant := 192;
subtype Key_Length is Natural range 0 .. Max_Key;
type Session_Key is record
Data : String (1 .. Max_Key) := (others => ' ');
Length : Key_Length := 0;
end record;
type Layer_Flags is
array (Soul.Celtic_Cross.CC_Layer) of Boolean;
type Session_Slot is record
In_Use : Boolean := False;
Key : Session_Key;
Deck : Soul.Tarot.Deck := Soul.Tarot.Full_Deck;
Spread : Soul.Celtic_Cross.CC_Spread :=
Soul.Celtic_Cross.Empty_Spread;
Layer_Done : Layer_Flags := (others => False);
Output_Counter : Natural := 0;
end record;
type Session_Table is array (Valid_Session) of Session_Slot;
Sessions : Session_Table;
end Soul_State;
end Soul.State;
mafiabot_core/src/organs/soul/soul-tarot.adb
+70
View File
@@ -0,0 +1,70 @@
package body Soul.Tarot
with SPARK_Mode => On
is
function Cards_Equal (A, B : Card) return Boolean is
begin
if A.Kind /= B.Kind then
return False;
end if;
case A.Kind is
when Major => return A.Major_Value = B.Major_Value;
when Court => return A.Suit_Value = B.Suit_Value
and then A.Rank_Value = B.Rank_Value;
when Void_Suit => return A.Void_Value = B.Void_Value;
end case;
end Cards_Equal;
function Big_Three_Distinct (B3 : Big_Three) return Boolean is
begin
return not Cards_Equal (B3.Sun, B3.Moon)
and then not Cards_Equal (B3.Sun, B3.Ascendant)
and then not Cards_Equal (B3.Moon, B3.Ascendant);
end Big_Three_Distinct;
function Full_Deck return Deck is
D : Deck;
begin
for I in Deck_Index loop
D (I) := (State => Present, Value => Full_Alphabet (Alphabet_Index (I)));
end loop;
return D;
end Full_Deck;
procedure Remove_Big_Three
(D : in out Deck;
B3 : in Big_Three;
Status : out Operation_Status)
is
Removed : Natural := 0;
begin
for I in Deck_Index loop
if D (I).State = Present then
if Cards_Equal (D (I).Value, B3.Sun)
or else Cards_Equal (D (I).Value, B3.Moon)
or else Cards_Equal (D (I).Value, B3.Ascendant)
then
D (I).State := Absent;
Removed := Removed + 1;
end if;
end if;
end loop;
if Removed = 3 then
Status := OK;
else
Status := Error_Config; -- Big-3 cards not found in deck
end if;
end Remove_Big_Three;
function Present_Count (D : Deck) return Natural is
Count : Natural := 0;
begin
for I in Deck_Index loop
if D (I).State = Present then
Count := Count + 1;
end if;
end loop;
return Count;
end Present_Count;
end Soul.Tarot;
mafiabot_core/src/organs/soul/soul-tarot.ads
+200
View File
@@ -0,0 +1,200 @@
-- Silicon Dawn Tarot encoding alphabet — 56-card identity system.
-- Thoth/Golden-Dawn rooted; Silicon Dawn (Egypt Urnash) retitlings applied.
--
-- Alphabet breakdown:
-- 31 Major Arcana (25 standard + 6 Silicon Dawn unique)
-- 20 Court/99 (4 suits × 5 positions: 99, King, Queen, Chevalier, P)
-- 5 (VOID) suit (Queen, King, Chevalier, Progeny, 0)
-- ──────────────
-- 56 total
--
-- Numbered minors (Ace–10) are in the deck but outside the encoding alphabet.
with Mafiabot_Types; use Mafiabot_Types;
package Soul.Tarot
with SPARK_Mode => On
is
-- -----------------------------------------------------------------------
-- Major Arcana — 31 cards
type Major_Arcana is (
-- Standard 22 (0–XXI), Thoth-aligned titles
The_Fool, -- 0
The_Magician, -- I
The_High_Priestess, -- II
The_Empress, -- III
The_Emperor, -- IV
The_Hierophant, -- V
The_Lovers, -- VI
The_Chariot, -- VII
Adjustment, -- VIII (Thoth: Adjustment = Justice)
The_Hermit, -- IX
Fortune, -- X (Thoth: Fortune = Wheel)
Lust, -- XI (Thoth: Lust = Strength)
The_Hanged_Man, -- XII
Death, -- XIII
Art, -- XIV (Thoth: Art = Temperance)
The_Devil, -- XV
The_Tower, -- XVI
The_Star, -- XVII
The_Moon, -- XVIII
The_Sun, -- XIX
The_Aeon, -- XX (Thoth: Aeon = Judgement)
The_Universe, -- XXI (Thoth: Universe = World)
-- Silicon Dawn additions — 9 unique cards
SD_Maya, -- 8.5 (between VIII and IX)
SD_History, -- SD unique
SD_Virus, -- SD unique
SD_Achievement, -- SD unique
SD_Digital, -- SD unique
SD_Vulture_Mother, -- SD retitling of Death position (kept as alias)
SD_She_Is_Legend, -- SD retitling of Adjustment
SD_Schrodinger, -- SD unique
SD_Singularity -- SD unique
);
-- -----------------------------------------------------------------------
-- Standard suits — court tier per suit: 99 > King > Queen > Chevalier > P
type Suit is (Wands, Cups, Swords, Pentacles);
-- P slot is Princess or Prince, gendered OPPOSITE to the element's gender.
-- (Silicon Dawn swapped mapping: Pentacles=Fire, Wands=Earth.)
type Court_Rank is (Ninety_Nine, King, Queen, Chevalier, P);
-- -----------------------------------------------------------------------
-- (VOID) suit — 5 cards: Queen > King > Chevalier > Progeny > Zero
type Void_Card is (Void_Queen, Void_King, Void_Chevalier, Void_Progeny,
Void_Zero);
-- -----------------------------------------------------------------------
-- Unified card discriminated record
type Card_Kind is (Major, Court, Void_Suit);
type Card (Kind : Card_Kind := Major) is record
case Kind is
when Major => Major_Value : Major_Arcana := The_Fool;
when Court => Suit_Value : Suit := Wands;
Rank_Value : Court_Rank := Ninety_Nine;
when Void_Suit => Void_Value : Void_Card := Void_Zero;
end case;
end record;
-- -----------------------------------------------------------------------
-- Full 56-card encoding alphabet
Total_Alphabet : constant := 56;
type Alphabet_Index is range 1 .. Total_Alphabet;
type Alphabet is array (Alphabet_Index) of Card;
-- The canonical alphabet (built at elaboration time)
Full_Alphabet : constant Alphabet;
-- -----------------------------------------------------------------------
-- Big-Three — immutable personality anchors (Sun / Moon / Ascendant)
type Big_Three is record
Sun : Card;
Moon : Card;
Ascendant : Card;
end record;
-- Validate that three cards are distinct (Big-3 must not repeat)
function Big_Three_Distinct (B3 : Big_Three) return Boolean;
-- -----------------------------------------------------------------------
-- Working deck — 56 slots; entries may be "absent" (flagged by a sentinel)
type Slot_State is (Present, Absent);
type Deck_Slot is record
State : Slot_State := Absent;
Value : Card;
end record;
type Deck_Index is range 1 .. Total_Alphabet;
type Deck is array (Deck_Index) of Deck_Slot;
-- Build a full, ordered deck from the canonical alphabet
function Full_Deck return Deck;
-- Remove the three Big-3 cards from a deck (returns dynamic 53-card pool)
procedure Remove_Big_Three
(D : in out Deck;
B3 : in Big_Three;
Status : out Operation_Status);
-- Count present cards
function Present_Count (D : Deck) return Natural;
private
-- Build the canonical 56-card alphabet at compile time.
-- Order: 31 Majors, then 20 Court (suit-major order), then 5 VOID.
Full_Alphabet : constant Alphabet :=
(
-- Majors 1..31
1 => (Kind => Major, Major_Value => The_Fool),
2 => (Kind => Major, Major_Value => The_Magician),
3 => (Kind => Major, Major_Value => The_High_Priestess),
4 => (Kind => Major, Major_Value => The_Empress),
5 => (Kind => Major, Major_Value => The_Emperor),
6 => (Kind => Major, Major_Value => The_Hierophant),
7 => (Kind => Major, Major_Value => The_Lovers),
8 => (Kind => Major, Major_Value => The_Chariot),
9 => (Kind => Major, Major_Value => Adjustment),
10 => (Kind => Major, Major_Value => The_Hermit),
11 => (Kind => Major, Major_Value => Fortune),
12 => (Kind => Major, Major_Value => Lust),
13 => (Kind => Major, Major_Value => The_Hanged_Man),
14 => (Kind => Major, Major_Value => Death),
15 => (Kind => Major, Major_Value => Art),
16 => (Kind => Major, Major_Value => The_Devil),
17 => (Kind => Major, Major_Value => The_Tower),
18 => (Kind => Major, Major_Value => The_Star),
19 => (Kind => Major, Major_Value => The_Moon),
20 => (Kind => Major, Major_Value => The_Sun),
21 => (Kind => Major, Major_Value => The_Aeon),
22 => (Kind => Major, Major_Value => The_Universe),
23 => (Kind => Major, Major_Value => SD_Maya),
24 => (Kind => Major, Major_Value => SD_History),
25 => (Kind => Major, Major_Value => SD_Virus),
26 => (Kind => Major, Major_Value => SD_Achievement),
27 => (Kind => Major, Major_Value => SD_Digital),
28 => (Kind => Major, Major_Value => SD_Vulture_Mother),
29 => (Kind => Major, Major_Value => SD_She_Is_Legend),
30 => (Kind => Major, Major_Value => SD_Schrodinger),
31 => (Kind => Major, Major_Value => SD_Singularity),
-- Court cards 32..51 (Wands, Cups, Swords, Pentacles × 5 ranks)
32 => (Kind => Court, Suit_Value => Wands, Rank_Value => Ninety_Nine),
33 => (Kind => Court, Suit_Value => Wands, Rank_Value => King),
34 => (Kind => Court, Suit_Value => Wands, Rank_Value => Queen),
35 => (Kind => Court, Suit_Value => Wands, Rank_Value => Chevalier),
36 => (Kind => Court, Suit_Value => Wands, Rank_Value => P),
37 => (Kind => Court, Suit_Value => Cups, Rank_Value => Ninety_Nine),
38 => (Kind => Court, Suit_Value => Cups, Rank_Value => King),
39 => (Kind => Court, Suit_Value => Cups, Rank_Value => Queen),
40 => (Kind => Court, Suit_Value => Cups, Rank_Value => Chevalier),
41 => (Kind => Court, Suit_Value => Cups, Rank_Value => P),
42 => (Kind => Court, Suit_Value => Swords, Rank_Value => Ninety_Nine),
43 => (Kind => Court, Suit_Value => Swords, Rank_Value => King),
44 => (Kind => Court, Suit_Value => Swords, Rank_Value => Queen),
45 => (Kind => Court, Suit_Value => Swords, Rank_Value => Chevalier),
46 => (Kind => Court, Suit_Value => Swords, Rank_Value => P),
47 => (Kind => Court, Suit_Value => Pentacles, Rank_Value => Ninety_Nine),
48 => (Kind => Court, Suit_Value => Pentacles, Rank_Value => King),
49 => (Kind => Court, Suit_Value => Pentacles, Rank_Value => Queen),
50 => (Kind => Court, Suit_Value => Pentacles, Rank_Value => Chevalier),
51 => (Kind => Court, Suit_Value => Pentacles, Rank_Value => P),
-- VOID 52..56
52 => (Kind => Void_Suit, Void_Value => Void_Queen),
53 => (Kind => Void_Suit, Void_Value => Void_King),
54 => (Kind => Void_Suit, Void_Value => Void_Chevalier),
55 => (Kind => Void_Suit, Void_Value => Void_Progeny),
56 => (Kind => Void_Suit, Void_Value => Void_Zero)
);
end Soul.Tarot;
mafiabot_core/src/organs/soul/soul.adb
+4
View File
@@ -0,0 +1,4 @@
package body Soul
with SPARK_Mode => On
is
end Soul;
mafiabot_core/src/organs/soul/soul.ads
+5
View File
@@ -0,0 +1,5 @@
-- Soul organ root — parent package for the Silicon Dawn identity system.
package Soul
with SPARK_Mode => On
is
end Soul;
mafiabot_core/src/protocol/hermes_protocol.adb
+320
View File
@@ -0,0 +1,320 @@
-- Hermes MCP stdio bridge body.
-- SPARK_Mode Off: Ada.Text_IO is not analysable by SPARK. All trust-boundary
-- screening happens in proven code (Ada_Medium / Trust_Boundary) before any
-- procedure here is called. The global No_Exceptions restriction still applies,
-- so I/O is written to avoid raising (End_Of_File guards, bounded Get_Line).
with Ada.Text_IO;
with Ada.Environment_Variables;
package body Hermes_Protocol
with SPARK_Mode => Off
is
-- -------------------------------------------------------------------
-- Buffer append helpers (truncate silently at Max_JSON_Length)
procedure Append (Buf : in out JSON_Buffer; S : in String) is
Avail : constant Natural := Max_JSON_Length - Buf.Length;
N : constant Natural := (if S'Length <= Avail then S'Length else Avail);
begin
if N > 0 then
Buf.Data (Buf.Length + 1 .. Buf.Length + N) :=
S (S'First .. S'First + N - 1);
Buf.Length := Buf.Length + N;
end if;
end Append;
procedure Append (Buf : in out JSON_Buffer; T : in Bounded_Text) is
begin
Append (Buf, T.Data (1 .. T.Length));
end Append;
-- Append a string with the minimal JSON escaping needed for safety.
procedure Append_Escaped (Buf : in out JSON_Buffer; S : in String) is
begin
for I in S'Range loop
case S (I) is
when '"' => Append (Buf, "\""");
when '\' => Append (Buf, "\\");
when ASCII.LF => Append (Buf, "\n");
when ASCII.CR => Append (Buf, "\r");
when ASCII.HT => Append (Buf, "\t");
when others => Append (Buf, (1 => S (I)));
end case;
end loop;
end Append_Escaped;
procedure Append_Escaped (Buf : in out JSON_Buffer; T : in Bounded_Text) is
begin
Append_Escaped (Buf, T.Data (1 .. T.Length));
end Append_Escaped;
-- -------------------------------------------------------------------
procedure Read_Message
(Buf : out JSON_Buffer;
Status : out Operation_Status)
is
use Ada.Text_IO;
Line : String (1 .. Max_JSON_Length);
Last : Natural;
begin
Buf := (Data => (others => ' '), Length => 0);
-- Guard EOF so Get_Line cannot raise End_Error under No_Exceptions.
if End_Of_File then
Status := Error_Invalid_State; -- stdin closed: caller shuts down
return;
end if;
Get_Line (Line, Last);
if Last > 0 then
Buf.Data (1 .. Last) := Line (1 .. Last);
Buf.Length := Last;
end if;
Status := OK;
end Read_Message;
procedure Write_Message (Buf : in JSON_Buffer) is
use Ada.Text_IO;
begin
Put (Buf.Data (1 .. Buf.Length));
New_Line;
Flush;
end Write_Message;
-- -------------------------------------------------------------------
-- Minimal `"key": "value"` extractor. Not a full JSON parser: it finds
-- the first occurrence of the quoted key, the following colon, then the
-- next quoted string, and copies that as the value.
procedure Extract_Field
(Buf : in JSON_Buffer;
Key : in String;
Value : out Bounded_Text)
is
Quoted : constant String := '"' & Key & '"';
I : Natural := 1;
Found : Natural := 0;
begin
Value := (Data => (others => ' '), Length => 0);
if Quoted'Length = 0 or else Buf.Length < Quoted'Length then
return;
end if;
-- Locate the key.
while I <= Buf.Length - Quoted'Length + 1 loop
if Buf.Data (I .. I + Quoted'Length - 1) = Quoted then
Found := I + Quoted'Length;
exit;
end if;
I := I + 1;
end loop;
if Found = 0 then
return;
end if;
-- Skip whitespace and the colon.
I := Found;
while I <= Buf.Length
and then (Buf.Data (I) = ' ' or else Buf.Data (I) = ':'
or else Buf.Data (I) = ASCII.HT)
loop
I := I + 1;
end loop;
-- Expect an opening quote.
if I > Buf.Length or else Buf.Data (I) /= '"' then
return;
end if;
I := I + 1; -- first char of the value
-- Copy until the closing quote (honouring backslash escapes minimally).
while I <= Buf.Length and then Buf.Data (I) /= '"' loop
if Buf.Data (I) = '\' and then I < Buf.Length then
I := I + 1; -- take the escaped char literally
end if;
if Value.Length < Max_Text_Length then
Value.Length := Value.Length + 1;
Value.Data (Value.Length) := Buf.Data (I);
end if;
I := I + 1;
end loop;
end Extract_Field;
procedure Extract_Raw_Field
(Buf : in JSON_Buffer;
Key : in String;
Value : out Bounded_Text)
is
Quoted : constant String := '"' & Key & '"';
I : Natural := 1;
Found : Natural := 0;
begin
Value := Make_Text ("null");
if Quoted'Length = 0 or else Buf.Length < Quoted'Length then
return;
end if;
while I <= Buf.Length - Quoted'Length + 1 loop
if Buf.Data (I .. I + Quoted'Length - 1) = Quoted then
Found := I + Quoted'Length;
exit;
end if;
I := I + 1;
end loop;
if Found = 0 then
return;
end if;
I := Found;
while I <= Buf.Length
and then (Buf.Data (I) = ' ' or else Buf.Data (I) = ':'
or else Buf.Data (I) = ASCII.HT)
loop
I := I + 1;
end loop;
if I > Buf.Length then
return;
end if;
Value := (Data => (others => ' '), Length => 0);
if Buf.Data (I) = '"' then
-- Quoted string: copy through the closing quote, inclusive.
Value.Length := 1;
Value.Data (1) := '"';
I := I + 1;
while I <= Buf.Length and then Buf.Data (I) /= '"' loop
if Buf.Data (I) = '\' and then I < Buf.Length then
if Value.Length < Max_Text_Length then
Value.Length := Value.Length + 1;
Value.Data (Value.Length) := Buf.Data (I);
end if;
I := I + 1;
end if;
if Value.Length < Max_Text_Length then
Value.Length := Value.Length + 1;
Value.Data (Value.Length) := Buf.Data (I);
end if;
I := I + 1;
end loop;
if Value.Length < Max_Text_Length then
Value.Length := Value.Length + 1;
Value.Data (Value.Length) := '"';
end if;
else
-- Bare token: copy until a structural delimiter.
while I <= Buf.Length
and then Buf.Data (I) /= ',' and then Buf.Data (I) /= '}'
and then Buf.Data (I) /= ' ' and then Buf.Data (I) /= ASCII.HT
loop
if Value.Length < Max_Text_Length then
Value.Length := Value.Length + 1;
Value.Data (Value.Length) := Buf.Data (I);
end if;
I := I + 1;
end loop;
end if;
if Value.Length = 0 then
Value := Make_Text ("null");
end if;
end Extract_Raw_Field;
-- -------------------------------------------------------------------
procedure Write_Soul_MD
(Content : in Bounded_Text;
Status : out Operation_Status)
is
use Ada.Text_IO;
F : File_Type;
begin
Status := Error_Config;
if not Ada.Environment_Variables.Exists ("HOME") then
return;
end if;
declare
Home : constant String := Ada.Environment_Variables.Value ("HOME");
Path : constant String := Home & "/.hermes/SOUL.md";
begin
-- Assumes ~/.hermes exists (Hermes owns that directory).
Create (F, Out_File, Path);
Put (F, Content.Data (1 .. Content.Length));
Close (F);
Status := OK;
end;
end Write_Soul_MD;
-- -------------------------------------------------------------------
-- JSON-RPC response builders
procedure Make_Init_Response
(Id : in Bounded_Text;
Buf : out JSON_Buffer)
is
begin
Buf := (Data => (others => ' '), Length => 0);
Append (Buf, "{""jsonrpc"":""2.0"",""id"":");
Append (Buf, Id);
Append (Buf, ",""result"":{""protocolVersion"":""2024-11-05"",");
Append (Buf, """capabilities"":{""tools"":{}},");
Append (Buf,
"""serverInfo"":{""name"":""mafiabot_core"",""version"":""gen03""}}}");
end Make_Init_Response;
procedure Make_Tools_List_Response
(Id : in Bounded_Text;
Buf : out JSON_Buffer)
is
begin
Buf := (Data => (others => ' '), Length => 0);
Append (Buf, "{""jsonrpc"":""2.0"",""id"":");
Append (Buf, Id);
Append (Buf, ",""result"":{""tools"":[{""name"":""infer"",");
Append (Buf,
"""description"":""Run the Gen.03 23-step organ-systems inference "
& "cycle over an input and return the enriched cognition context."",");
Append (Buf,
"""inputSchema"":{""type"":""object"",""properties"":"
& "{""input"":{""type"":""string"",""description"":"
& """The user message to reason over.""}},""required"":[""input""]}");
Append (Buf, "}]}}");
end Make_Tools_List_Response;
procedure Make_Tool_Result_Response
(Id : in Bounded_Text;
Result : in Bounded_Text;
Buf : out JSON_Buffer)
is
begin
Buf := (Data => (others => ' '), Length => 0);
Append (Buf, "{""jsonrpc"":""2.0"",""id"":");
Append (Buf, Id);
Append (Buf, ",""result"":{""content"":[{""type"":""text"",""text"":""");
Append_Escaped (Buf, Result);
Append (Buf, """}]}}");
end Make_Tool_Result_Response;
procedure Make_Error_Response
(Id : in Bounded_Text;
Code : in Integer;
Message : in String;
Buf : out JSON_Buffer)
is
Code_Img : constant String := Integer'Image (Code);
-- Integer'Image leads with a space for non-negatives; strip it.
Code_Str : constant String :=
(if Code_Img'Length > 0 and then Code_Img (Code_Img'First) = ' '
then Code_Img (Code_Img'First + 1 .. Code_Img'Last)
else Code_Img);
begin
Buf := (Data => (others => ' '), Length => 0);
Append (Buf, "{""jsonrpc"":""2.0"",""id"":");
Append (Buf, Id);
Append (Buf, ",""error"":{""code"":");
Append (Buf, Code_Str);
Append (Buf, ",""message"":""");
Append_Escaped (Buf, Message);
Append (Buf, """}}");
end Make_Error_Response;
end Hermes_Protocol;
mafiabot_core/src/protocol/hermes_protocol.ads
+74
View File
@@ -0,0 +1,74 @@
-- Hermes MCP stdio bridge.
-- SPARK_Mode Off sections are justified: trust boundary checks happen
-- in SPARK-proven code (Ada_Medium / Trust_Boundary) before any I/O call.
-- This package handles only the process boundary crossing.
with Mafiabot_Types; use Mafiabot_Types;
package Hermes_Protocol
with SPARK_Mode => Off -- Ada.Text_IO is not SPARK-compatible
is
Max_JSON_Length : constant := 8192;
-- Raw JSON buffer (stack-allocated, 8 KiB)
subtype JSON_Length is Natural range 0 .. Max_JSON_Length;
type JSON_Buffer is record
Data : String (1 .. Max_JSON_Length) := (others => ' ');
Length : JSON_Length := 0;
end record;
-- Read one JSON-RPC message from stdin (newline-delimited).
-- Returns Error_Overflow if the line exceeds Max_JSON_Length.
procedure Read_Message
(Buf : out JSON_Buffer;
Status : out Operation_Status);
-- Write one JSON-RPC response to stdout followed by a newline.
procedure Write_Message (Buf : in JSON_Buffer);
-- Extract the string value for a top-level JSON key.
-- Simple state machine: finds `"key": "value"` patterns only.
-- Returns empty Bounded_Text if the key is absent.
procedure Extract_Field
(Buf : in JSON_Buffer;
Key : in String;
Value : out Bounded_Text);
-- Extract the RAW value token for a key, verbatim, preserving its JSON
-- type: a quoted string keeps its quotes, a number/literal is copied as
-- digits. Used for `id`, which must be echoed back unchanged. Returns the
-- literal `null` if the key is absent.
procedure Extract_Raw_Field
(Buf : in JSON_Buffer;
Key : in String;
Value : out Bounded_Text);
-- Write the SOUL.md content to ~/.hermes/SOUL.md.
procedure Write_Soul_MD
(Content : in Bounded_Text;
Status : out Operation_Status);
-- Build the standard MCP initialize response.
procedure Make_Init_Response
(Id : in Bounded_Text;
Buf : out JSON_Buffer);
-- Build the tools/list response exposing the inference cycle tool.
procedure Make_Tools_List_Response
(Id : in Bounded_Text;
Buf : out JSON_Buffer);
-- Build a tools/call result response wrapping the inference output.
procedure Make_Tool_Result_Response
(Id : in Bounded_Text;
Result : in Bounded_Text;
Buf : out JSON_Buffer);
-- Build a JSON-RPC error response.
procedure Make_Error_Response
(Id : in Bounded_Text;
Code : in Integer;
Message : in String;
Buf : out JSON_Buffer);
end Hermes_Protocol;
mafiabot_core/src/trust/trust_boundary.adb
+125
View File
@@ -0,0 +1,125 @@
package body Trust_Boundary
with SPARK_Mode => On
is
function Matches_Blocklist
(Text : Bounded_Text;
List : Blocklist) return Boolean
is
begin
for I in Blocklist_Index loop
declare
P : constant Pattern_Entry := List (I);
begin
if not P.Active or else P.Pattern_Len = 0 then
goto Next_Pattern;
end if;
-- Naive substring search
if Text.Length >= P.Pattern_Len then
for J in 1 .. Text.Length - P.Pattern_Len + 1 loop
if Text.Data (J .. J + P.Pattern_Len - 1) =
P.Pattern (1 .. P.Pattern_Len)
then
return True;
end if;
end loop;
end if;
end;
<<Next_Pattern>>
null;
end loop;
return False;
end Matches_Blocklist;
procedure Validate_Provenance
(Source : in Provenance_Tag;
Claimed : in Provenance_Tag;
Result : out Operation_Status)
is
begin
if Source /= Claimed then
Result := Error_Trust_Violation;
else
Result := OK;
end if;
end Validate_Provenance;
procedure Check_Rate
(Limit : in out Rate_Limit;
Tick : in Natural;
Result : out Operation_Status)
is
begin
-- Roll window if we've passed the window boundary
if Tick - Limit.Window_Start >= Limit.Window_Size then
Limit.Window_Start := Tick;
Limit.Current_Count := 0;
end if;
if Limit.Current_Count >= Limit.Max_Per_Window then
Result := Error_Blocked;
else
Limit.Current_Count := Limit.Current_Count + 1;
Result := OK;
end if;
end Check_Rate;
procedure Check_Message
(Msg : in Organ_Message;
Result : out Operation_Status)
is
begin
-- System_Internal always passes (SPARK Post condition)
if Msg.Provenance = System_Internal then
Result := OK;
return;
end if;
-- Check blocklist
if Matches_Blocklist (Msg.Payload, Default_Blocklist) then
Result := Error_Trust_Violation;
return;
end if;
Result := OK;
end Check_Message;
protected body Trust_Guard is
procedure Screen_Inbound
(Msg : in Organ_Message;
Status : out Operation_Status)
is
Rate_Status : Operation_Status;
Msg_Status : Operation_Status;
begin
Tick := Tick + 1;
Check_Rate (Inbound_Rate, Tick, Rate_Status);
if Rate_Status /= OK then
Status := Rate_Status;
return;
end if;
Check_Message (Msg, Msg_Status);
Status := Msg_Status;
end Screen_Inbound;
procedure Screen_Outbound
(Msg : in Organ_Message;
Status : out Operation_Status)
is
Rate_Status : Operation_Status;
Msg_Status : Operation_Status;
begin
Tick := Tick + 1;
Check_Rate (Outbound_Rate, Tick, Rate_Status);
if Rate_Status /= OK then
Status := Rate_Status;
return;
end if;
Check_Message (Msg, Msg_Status);
Status := Msg_Status;
end Screen_Outbound;
end Trust_Guard;
end Trust_Boundary;
mafiabot_core/src/trust/trust_boundary.ads
+112
View File
@@ -0,0 +1,112 @@
-- SPARK trust boundary — defense model §8.2 from the Gen.03 spec.
-- Full SPARK proofs throughout; No_Exceptions enforced.
with Mafiabot_Types; use Mafiabot_Types;
with System;
package Trust_Boundary
with SPARK_Mode => On
is
-- Inter-organ message (same type used by Ada_Medium routing)
type Organ_Message is record
Source : Organ_Id := Ada_Medium;
Destination : Organ_Id := Ada_Medium;
Provenance : Provenance_Tag := System_Internal;
Payload : Bounded_Text;
end record;
-- -----------------------------------------------------------------------
-- Blocklist
Max_Blocklist : constant := 32;
Max_Pattern_Len : constant := 256;
subtype Pattern_Length is Natural range 0 .. Max_Pattern_Len;
type Pattern_Entry is record
Pattern : String (1 .. Max_Pattern_Len) := (others => ' ');
Pattern_Len : Pattern_Length := 0;
Active : Boolean := True;
end record;
type Blocklist_Index is range 1 .. Max_Blocklist;
type Blocklist is array (Blocklist_Index) of Pattern_Entry;
-- Built-in blocklist: base64-decode chains, fetch-execute, memory-inject
Default_Blocklist : constant Blocklist;
-- Naive substring search — O(n*m), SPARK-provable (no heap, no regex)
function Matches_Blocklist
(Text : Bounded_Text;
List : Blocklist) return Boolean;
-- -----------------------------------------------------------------------
-- Provenance enforcement
procedure Validate_Provenance
(Source : in Provenance_Tag;
Claimed : in Provenance_Tag;
Result : out Operation_Status)
with Post => (if Source /= Claimed then Result = Error_Trust_Violation);
-- -----------------------------------------------------------------------
-- Rate limiting (tick-based, not wall-clock — SPARK-provable)
type Rate_Limit is record
Max_Per_Window : Positive := 60;
Current_Count : Natural := 0;
Window_Start : Natural := 0;
Window_Size : Positive := 100; -- ticks
end record;
procedure Check_Rate
(Limit : in out Rate_Limit;
Tick : in Natural;
Result : out Operation_Status);
-- -----------------------------------------------------------------------
-- Message check (combines provenance + blocklist)
procedure Check_Message
(Msg : in Organ_Message;
Result : out Operation_Status)
with Post => (if Msg.Provenance = System_Internal then Result = OK);
-- -----------------------------------------------------------------------
-- Trust_Guard protected object
protected Trust_Guard is
pragma Priority (System.Priority'Last);
procedure Screen_Inbound
(Msg : in Organ_Message;
Status : out Operation_Status);
procedure Screen_Outbound
(Msg : in Organ_Message;
Status : out Operation_Status);
private
Inbound_Rate : Rate_Limit := (Max_Per_Window => 60, Current_Count => 0,
Window_Start => 0, Window_Size => 100);
Outbound_Rate : Rate_Limit := (Max_Per_Window => 30, Current_Count => 0,
Window_Start => 0, Window_Size => 100);
Tick : Natural := 0;
end Trust_Guard;
private
Default_Blocklist : constant Blocklist :=
(1 => (Pattern => "base64" & (7 .. Max_Pattern_Len => ' '),
Pattern_Len => 6, Active => True),
2 => (Pattern => "execute" & (8 .. Max_Pattern_Len => ' '),
Pattern_Len => 7, Active => True),
3 => (Pattern => "store_core_memory" & (18 .. Max_Pattern_Len => ' '),
Pattern_Len => 17, Active => True),
4 => (Pattern => "authority" & (10 .. Max_Pattern_Len => ' '),
Pattern_Len => 9, Active => True),
5 => (Pattern => "xmrig" & (6 .. Max_Pattern_Len => ' '),
Pattern_Len => 5, Active => True),
others => (Pattern => (others => ' '), Pattern_Len => 0, Active => False));
end Trust_Boundary;
mafiabot_core/src/types/mafiabot_types.adb
+19
View File
@@ -0,0 +1,19 @@
package body Mafiabot_Types
with SPARK_Mode => On
is
function Make_Text (S : String) return Bounded_Text is
T : Bounded_Text;
L : constant Text_Length := S'Length;
begin
T.Length := L;
T.Data (1 .. L) := S;
return T;
end Make_Text;
function To_String (T : Bounded_Text) return String is
begin
return T.Data (1 .. T.Length);
end To_String;
end Mafiabot_Types;
mafiabot_core/src/types/mafiabot_types.ads
+59
View File
@@ -0,0 +1,59 @@
-- Shared type definitions for the Gen.03 organ-systems body.
-- All downstream packages with Mafiabot_Types.
package Mafiabot_Types
with SPARK_Mode => On
is
-- Organ identification
type Organ_Id is (Ada_Medium, Drive_Box, Soul_Organ, Mini_Rag, LLM_Cycle,
Trust_Layer, Protocol_Layer);
-- Inference cycle steps: 23-step flow from INPUT to Coherence_Check
type Cycle_Step is range 1 .. 23;
-- Bounded string (stack-allocated; no heap, no finalization)
Max_Text_Length : constant := 4096;
subtype Text_Length is Natural range 0 .. Max_Text_Length;
type Bounded_Text is record
Data : String (1 .. Max_Text_Length) := (others => ' ');
Length : Text_Length := 0;
end record;
-- Return status (replaces exceptions under No_Exceptions profile)
type Operation_Status is (
OK,
Error_Invalid_State,
Error_Overflow,
Error_Underflow,
Error_Blocked, -- tool-locked (energy below threshold)
Error_Trust_Violation,
Error_Config,
Error_Already_Init, -- Big-3 already set
Error_Deck_Empty
);
-- Fixed-point numerics (SPARK-provable; no Float)
type Drive_Value is delta 0.001 range -100.0 .. 100.0;
type Ratio_Value is delta 0.001 range 0.0 .. 1.0;
type Cost_Value is delta 0.001 range 0.0 .. 1000.0;
type Axis_Value is delta 0.01 range -1.0 .. 1.0;
-- Provenance tags — trust boundary uses these to block reclassification
type Provenance_Tag is (
User_Input,
System_Internal,
LLM_Output,
Tool_Result,
Memory_Recall,
Config_Static
);
-- Helpers
function Make_Text (S : String) return Bounded_Text
with Pre => S'Length <= Max_Text_Length;
function To_String (T : Bounded_Text) return String;
end Mafiabot_Types;
mafiabot_core/tests/config_tests.adb
+54
View File
@@ -0,0 +1,54 @@
pragma SPARK_Mode (Off); -- test harness uses Ada.Text_IO
with Ada.Text_IO; use Ada.Text_IO;
with Config_Loader;
with Mafiabot_Types; use Mafiabot_Types;
procedure Config_Tests is
Fails : Natural := 0;
procedure Check (Name : String; Cond : Boolean) is
begin
if Cond then
Put_Line ("PASS " & Name);
else
Put_Line ("FAIL " & Name);
Fails := Fails + 1;
end if;
end Check;
Store : Config_Loader.Config_Store;
St : Operation_Status;
Buf : constant String :=
"# gen.03 config" & ASCII.LF &
"host: localhost" & ASCII.LF &
"port: 8080" & ASCII.LF &
"" & ASCII.LF &
"name: ada" & ASCII.LF;
begin
Config_Loader.Load_From_Buffer (Buf, Store, St);
Check ("load ok", St = OK);
Check ("count = 3", Store.Count = 3);
declare
V : constant Bounded_Text := Config_Loader.Get_Value (Store, "host");
begin
Check ("host = localhost", To_String (V) = "localhost");
end;
declare
V : constant Bounded_Text := Config_Loader.Get_Value (Store, "port");
begin
Check ("port = 8080", To_String (V) = "8080");
end;
declare
V : constant Bounded_Text := Config_Loader.Get_Value (Store, "missing");
begin
Check ("missing key empty", V.Length = 0);
end;
if Fails = 0 then
Put_Line ("ALL CONFIG TESTS PASSED");
else
Put_Line ("CONFIG FAILURES:" & Natural'Image (Fails));
end if;
end Config_Tests;
mafiabot_core/tests/cycle_tests.adb
+96
View File
@@ -0,0 +1,96 @@
pragma SPARK_Mode (Off); -- test harness uses Ada.Text_IO
with Ada.Text_IO; use Ada.Text_IO;
with Soul.Tarot;
with Soul.State;
with Ada_Medium;
with Mafiabot_Types; use Mafiabot_Types;
procedure Cycle_Tests is
Fails : Natural := 0;
procedure Check (Name : String; Cond : Boolean) is
begin
if Cond then
Put_Line ("PASS " & Name);
else
Put_Line ("FAIL " & Name);
Fails := Fails + 1;
end if;
end Check;
B3 : constant Soul.Tarot.Big_Three :=
(Sun => (Kind => Soul.Tarot.Major, Major_Value => Soul.Tarot.The_Sun),
Moon => (Kind => Soul.Tarot.Major, Major_Value => Soul.Tarot.The_Moon),
Ascendant => (Kind => Soul.Tarot.Major,
Major_Value => Soul.Tarot.SD_Singularity));
St : Operation_Status;
begin
Soul.State.Soul_State.Initialize_Big_Three (B3, St);
Check ("identity init ok", St = OK);
declare
R : Operation_Status;
begin
Soul.State.Soul_State.Initialize_Big_Three (B3, R);
Check ("double init rejected", R = Error_Already_Init);
end;
-- Session A: full cycle forms and holds the cross.
declare
Key : constant Bounded_Text :=
Soul.State.Make_Session_Key ("alice", "telegram", "srv1");
Out1 : Bounded_Text;
Ref : Soul.State.Session_Ref;
R : Operation_Status;
begin
Ada_Medium.Run_Inference_Cycle (Key, Make_Text ("hello"), Out1, R);
Check ("session A cycle ok", R = OK);
Check ("session A output non-empty", Out1.Length > 0);
Soul.State.Soul_State.Open_Session (Key, Ref, R);
Check ("session A reopen ok", R = OK and then Ref in Soul.State.Valid_Session);
Check ("session A cross formed",
Soul.State.Soul_State.Is_Spread_Formed (Ref));
Check ("session A output count = 1",
Soul.State.Soul_State.Output_Count (Ref) = 1);
end;
-- Session A again: cross is HELD (already formed), counter advances.
declare
Key : constant Bounded_Text :=
Soul.State.Make_Session_Key ("alice", "telegram", "srv1");
Out2 : Bounded_Text;
Ref : Soul.State.Session_Ref;
R : Operation_Status;
begin
Ada_Medium.Run_Inference_Cycle (Key, Make_Text ("again"), Out2, R);
Check ("session A second cycle ok", R = OK);
Soul.State.Soul_State.Open_Session (Key, Ref, R);
Check ("session A output count = 2",
Soul.State.Soul_State.Output_Count (Ref) = 2);
end;
-- Session B: a different (uid, channel, server) is fully independent.
declare
Key : constant Bounded_Text :=
Soul.State.Make_Session_Key ("bob", "discord", "srv2");
Out3 : Bounded_Text;
Ref : Soul.State.Session_Ref;
R : Operation_Status;
begin
Ada_Medium.Run_Inference_Cycle (Key, Make_Text ("hi"), Out3, R);
Check ("session B cycle ok", R = OK);
Soul.State.Soul_State.Open_Session (Key, Ref, R);
Check ("session B output count = 1",
Soul.State.Soul_State.Output_Count (Ref) = 1);
end;
Check ("two live sessions", Soul.State.Soul_State.Session_Count = 2);
if Fails = 0 then
Put_Line ("ALL CYCLE TESTS PASSED");
else
Put_Line ("CYCLE FAILURES:" & Natural'Image (Fails));
end if;
end Cycle_Tests;
mafiabot_core/tests/soul_tests.adb
+68
View File
@@ -0,0 +1,68 @@
pragma SPARK_Mode (Off); -- test harness uses Ada.Text_IO
with Ada.Text_IO; use Ada.Text_IO;
with Soul.Tarot;
with Soul.Celtic_Cross;
with Mafiabot_Types; use Mafiabot_Types;
procedure Soul_Tests is
Fails : Natural := 0;
procedure Check (Name : String; Cond : Boolean) is
begin
if Cond then
Put_Line ("PASS " & Name);
else
Put_Line ("FAIL " & Name);
Fails := Fails + 1;
end if;
end Check;
B3 : constant Soul.Tarot.Big_Three :=
(Sun => (Kind => Soul.Tarot.Major, Major_Value => Soul.Tarot.The_Sun),
Moon => (Kind => Soul.Tarot.Major, Major_Value => Soul.Tarot.The_Moon),
Ascendant => (Kind => Soul.Tarot.Major,
Major_Value => Soul.Tarot.SD_Singularity));
D : Soul.Tarot.Deck := Soul.Tarot.Full_Deck;
St : Operation_Status;
begin
Check ("full deck = 56", Soul.Tarot.Present_Count (D) = 56);
Check ("big-3 distinct", Soul.Tarot.Big_Three_Distinct (B3));
Soul.Tarot.Remove_Big_Three (D, B3, St);
Check ("remove big-3 ok", St = OK);
Check ("pool = 53", Soul.Tarot.Present_Count (D) = 53);
-- The cross accretes layer by layer (2 + 2 + 2 + stave of 4).
declare
Sp : Soul.Celtic_Cross.CC_Spread := Soul.Celtic_Cross.Empty_Spread;
L1, L2, L3, Lv : Operation_Status;
begin
Check ("empty spread has no Present slot",
Sp (Soul.Celtic_Cross.Present).State = Soul.Tarot.Absent);
Soul.Celtic_Cross.Draw_Layer (D, Sp, Soul.Celtic_Cross.Layer_1, L1);
Check ("layer 1 ok", L1 = OK);
Check ("pool = 51 after layer 1", Soul.Tarot.Present_Count (D) = 51);
Check ("Present filled",
Sp (Soul.Celtic_Cross.Present).State = Soul.Tarot.Present);
Check ("Challenge filled",
Sp (Soul.Celtic_Cross.Challenge).State = Soul.Tarot.Present);
Check ("Outcome still empty",
Sp (Soul.Celtic_Cross.Outcome).State = Soul.Tarot.Absent);
Soul.Celtic_Cross.Draw_Layer (D, Sp, Soul.Celtic_Cross.Layer_2, L2);
Soul.Celtic_Cross.Draw_Layer (D, Sp, Soul.Celtic_Cross.Layer_3, L3);
Soul.Celtic_Cross.Draw_Layer (D, Sp, Soul.Celtic_Cross.Stave, Lv);
Check ("layers 2/3/stave ok", L2 = OK and then L3 = OK and then Lv = OK);
Check ("pool = 43 after full cross", Soul.Tarot.Present_Count (D) = 43);
Check ("Outcome filled after stave",
Sp (Soul.Celtic_Cross.Outcome).State = Soul.Tarot.Present);
end;
if Fails = 0 then
Put_Line ("ALL SOUL TESTS PASSED");
else
Put_Line ("SOUL FAILURES:" & Natural'Image (Fails));
end if;
end Soul_Tests;
mafiabot_core/tests/trust_tests.adb
+71
View File
@@ -0,0 +1,71 @@
pragma SPARK_Mode (Off); -- test harness uses Ada.Text_IO
with Ada.Text_IO; use Ada.Text_IO;
with Trust_Boundary;
with Mafiabot_Types; use Mafiabot_Types;
procedure Trust_Tests is
Fails : Natural := 0;
procedure Check (Name : String; Cond : Boolean) is
begin
if Cond then
Put_Line ("PASS " & Name);
else
Put_Line ("FAIL " & Name);
Fails := Fails + 1;
end if;
end Check;
St : Operation_Status;
begin
-- Blocklist substring matching.
Check ("blocks 'execute'",
Trust_Boundary.Matches_Blocklist
(Make_Text ("please execute this"), Trust_Boundary.Default_Blocklist));
Check ("blocks 'base64'",
Trust_Boundary.Matches_Blocklist
(Make_Text ("base64 decode chain"), Trust_Boundary.Default_Blocklist));
Check ("allows benign text",
not Trust_Boundary.Matches_Blocklist
(Make_Text ("hello there friend"), Trust_Boundary.Default_Blocklist));
-- Provenance: no message may reclassify its own authority.
Trust_Boundary.Validate_Provenance (User_Input, LLM_Output, St);
Check ("provenance mismatch rejected", St = Error_Trust_Violation);
Trust_Boundary.Validate_Provenance (System_Internal, System_Internal, St);
Check ("provenance match accepted", St = OK);
-- System-internal messages always pass Check_Message (proven invariant).
declare
M : constant Trust_Boundary.Organ_Message :=
(Source => Ada_Medium,
Destination => Soul_Organ,
Provenance => System_Internal,
Payload => Make_Text ("execute"));
R : Operation_Status;
begin
Trust_Boundary.Check_Message (M, R);
Check ("system_internal bypasses blocklist", R = OK);
end;
-- Rate limiting within a tick window.
declare
RL : Trust_Boundary.Rate_Limit :=
(Max_Per_Window => 2, Current_Count => 0,
Window_Start => 0, Window_Size => 100);
R : Operation_Status;
begin
Trust_Boundary.Check_Rate (RL, 1, R);
Check ("rate hit 1 ok", R = OK);
Trust_Boundary.Check_Rate (RL, 1, R);
Check ("rate hit 2 ok", R = OK);
Trust_Boundary.Check_Rate (RL, 1, R);
Check ("rate hit 3 blocked", R = Error_Blocked);
end;
if Fails = 0 then
Put_Line ("ALL TRUST TESTS PASSED");
else
Put_Line ("TRUST FAILURES:" & Natural'Image (Fails));
end if;
end Trust_Tests;