diff --git a/mafiabot_core/alire.toml b/mafiabot_core/alire.toml index 6287368..a866db7 100644 --- a/mafiabot_core/alire.toml +++ b/mafiabot_core/alire.toml @@ -8,9 +8,9 @@ maintainers-logins = ["sybad"] # here, and neither "Proprietary TBD" nor a LicenseRef- custom id is accepted by # the pinned Alire, so the (optional) field is left out until a license is chosen. -[[depends-on]] -gnat_sockets = "^1.0.0" -spark_lemmas = "^1.0.0" +# No external crate deps: nothing here `with`s GNAT.Sockets or SPARK.Lemmas. +# (They were declared for the deleted sockets stub and never used.) Re-add as +# real needs appear. # Build modes wildcard "*". Restrictions are NOT a build-switch: see gnat.adc. [build-switches] diff --git a/mafiabot_core/mafiabot_core.gpr b/mafiabot_core/mafiabot_core.gpr index ba72095..b9bf5e9 100644 --- a/mafiabot_core/mafiabot_core.gpr +++ b/mafiabot_core/mafiabot_core.gpr @@ -2,28 +2,25 @@ with "config/mafiabot_core_config.gpr"; project Mafiabot_Core is + -- Only directories that actually hold Ada sources. The old organ/network + -- stubs (soul tarot, ada_medium, sockets) are gone — that cognition is + -- moving to Ichor (Pony) and the R/Octave organs. for Source_Dirs use - ("src", - "src/core", - "src/daemons", - "src/network", - "src/payloads", - "src/types", + ("src/core", "src/config_loader", "src/trust", - "src/organs/soul", - "src/organs/ada_medium", "src/protocol", + "src/types", "config", "tests"); for Object_Dir use "obj"; for Exec_Dir use "bin"; + + -- Test harnesses only. There is no application main yet (mafiabot.adb was + -- never written); add it here when it exists. for Main use - ("mafiabot.adb", - "engine_tests.adb", - "soul_tests.adb", + ("engine_tests.adb", "trust_tests.adb", - "cycle_tests.adb", "config_tests.adb"); package Builder is diff --git a/mafiabot_core/src/network/sockets.adb b/mafiabot_core/src/network/sockets.adb deleted file mode 100644 index 6de6778..0000000 --- a/mafiabot_core/src/network/sockets.adb +++ /dev/null @@ -1,2 +0,0 @@ -package body Sockets is -end Sockets; diff --git a/mafiabot_core/src/network/sockets.ads b/mafiabot_core/src/network/sockets.ads deleted file mode 100644 index b8557a7..0000000 --- a/mafiabot_core/src/network/sockets.ads +++ /dev/null @@ -1,2 +0,0 @@ -package Sockets is -end Sockets; diff --git a/mafiabot_core/src/organs/ada_medium/ada_medium.adb b/mafiabot_core/src/organs/ada_medium/ada_medium.adb deleted file mode 100644 index 0b34bd6..0000000 --- a/mafiabot_core/src/organs/ada_medium/ada_medium.adb +++ /dev/null @@ -1,344 +0,0 @@ --- with Soul.State; --- --- package body Ada_Medium --- with SPARK_Mode => On --- is --- WRONG ASK ME WHY - -- 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 := (Data => (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; - -- Qualify the Organ_Id literal: the simple name Ada_Medium binds to - -- this package, shadowing the enum value of the same name. - Msg := Make_Internal_Msg - (Mafiabot_Types.Ada_Medium, Mafiabot_Types.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; diff --git a/mafiabot_core/src/organs/soul/bbb-bludbrenburier.ads b/mafiabot_core/src/organs/soul/bbb-bludbrenburier.ads deleted file mode 100644 index f84af69..0000000 --- a/mafiabot_core/src/organs/soul/bbb-bludbrenburier.ads +++ /dev/null @@ -1 +0,0 @@ --- this is filler \ No newline at end of file diff --git a/mafiabot_core/src/trust/invariants-architecture.cobol b/mafiabot_core/src/trust/invariants-architecture.cobol deleted file mode 100644 index 5c17e45..0000000 --- a/mafiabot_core/src/trust/invariants-architecture.cobol +++ /dev/null @@ -1 +0,0 @@ -idk cobol \ No newline at end of file diff --git a/mafiabot_core/src/trust/trust_boundary.adb b/mafiabot_core/src/trust/trust_boundary.adb new file mode 100644 index 0000000..cdc37b8 --- /dev/null +++ b/mafiabot_core/src/trust/trust_boundary.adb @@ -0,0 +1,131 @@ +-- SPARK trust boundary body — defense model §8.2. +-- No heap, no regex, no exceptions: naive substring search, tick-based rate +-- limiting, provenance equality. Matches the contracts in the spec. +package body Trust_Boundary + with SPARK_Mode => On +is + + -- -------------------------------------------------------------------- + -- Naive substring search — O(n*m), no heap, no regex. + + function Matches_Blocklist + (Text : Bounded_Text; + List : Blocklist) return Boolean + is + begin + for I in Blocklist_Index loop + if List (I).Active and then List (I).Pattern_Len > 0 + and then List (I).Pattern_Len <= Text.Length + then + declare + P_Len : constant Pattern_Length := List (I).Pattern_Len; + Pat : constant String := List (I).Pattern (1 .. P_Len); + begin + for Start in 1 .. (Text.Length - P_Len + 1) loop + if Text.Data (Start .. Start + P_Len - 1) = Pat then + return True; + end if; + end loop; + end; + end if; + end loop; + return False; + end Matches_Blocklist; + + -- -------------------------------------------------------------------- + -- Provenance enforcement: a message may not reclassify its authority. + + procedure Validate_Provenance + (Source : in Provenance_Tag; + Claimed : in Provenance_Tag; + Result : out Operation_Status) + is + begin + if Source = Claimed then + Result := OK; + else + Result := Error_Trust_Violation; + end if; + end Validate_Provenance; + + -- -------------------------------------------------------------------- + -- Tick-based rate limiting (no wall-clock). + + procedure Check_Rate + (Limit : in out Rate_Limit; + Tick : in Natural; + Result : out Operation_Status) + is + begin + -- Open a fresh window if the clock reset or the window has elapsed. + if Tick < Limit.Window_Start + or else (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 + Limit.Current_Count := Limit.Current_Count + 1; + Result := OK; + else + Result := Error_Blocked; + end if; + end Check_Rate; + + -- -------------------------------------------------------------------- + -- Combined message check: system-internal always passes (proven + -- invariant); everything else is screened against the blocklist. + + procedure Check_Message + (Msg : in Border_Message; + Result : out Operation_Status) + is + begin + if Msg.Provenance = System_Internal then + Result := OK; + elsif Matches_Blocklist (Msg.Payload, Default_Blocklist) then + Result := Error_Blocked; + else + Result := OK; + end if; + end Check_Message; + + -- -------------------------------------------------------------------- + -- The guard: rate-limit then screen, on a shared tick. + + protected body Trust_Guard is + + procedure Screen_Inbound + (Msg : in Border_Message; + Status : out Operation_Status) + is + Rate_Status : Operation_Status; + begin + Tick := Tick + 1; + Check_Rate (Inbound_Rate, Tick, Rate_Status); + if Rate_Status /= OK then + Status := Rate_Status; + else + Check_Message (Msg, Status); + end if; + end Screen_Inbound; + + procedure Screen_Outbound + (Msg : in Border_Message; + Status : out Operation_Status) + is + Rate_Status : Operation_Status; + begin + Tick := Tick + 1; + Check_Rate (Outbound_Rate, Tick, Rate_Status); + if Rate_Status /= OK then + Status := Rate_Status; + else + Check_Message (Msg, Status); + end if; + end Screen_Outbound; + + end Trust_Guard; + +end Trust_Boundary; diff --git a/mafiabot_core/src/trust/trust_boundary.ads b/mafiabot_core/src/trust/trust_boundary.ads index af8184e..e365488 100644 --- a/mafiabot_core/src/trust/trust_boundary.ads +++ b/mafiabot_core/src/trust/trust_boundary.ads @@ -7,12 +7,12 @@ 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; + -- A message crossing the border (D1). Ada does not route by organ -- that + -- is Ichor's job -- so this carries only the source/trust tag the gate + -- screens by, plus the (pre-digested) payload to scan. + type Border_Message is record + Provenance : Provenance_Tag := System_Internal; + Payload : Bounded_Text; end record; -- ----------------------------------------------------------------------- @@ -68,7 +68,7 @@ is -- Message check (combines provenance + blocklist) procedure Check_Message - (Msg : in Organ_Message; + (Msg : in Border_Message; Result : out Operation_Status) with Post => (if Msg.Provenance = System_Internal then Result = OK); @@ -79,11 +79,11 @@ is pragma Priority (System.Priority'Last); procedure Screen_Inbound - (Msg : in Organ_Message; + (Msg : in Border_Message; Status : out Operation_Status); procedure Screen_Outbound - (Msg : in Organ_Message; + (Msg : in Border_Message; Status : out Operation_Status); private diff --git a/mafiabot_core/src/types/mafiabot_types.adb b/mafiabot_core/src/types/mafiabot_types.adb new file mode 100644 index 0000000..c58e4fc --- /dev/null +++ b/mafiabot_core/src/types/mafiabot_types.adb @@ -0,0 +1,21 @@ +-- Bodies for the shared helpers declared in Mafiabot_Types. +package body Mafiabot_Types + with SPARK_Mode => On +is + + function Make_Text (S : String) return Bounded_Text is + Result : Bounded_Text; + begin + Result.Length := S'Length; + if S'Length > 0 then + Result.Data (1 .. S'Length) := S; + end if; + return Result; + 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; diff --git a/mafiabot_core/src/types/mafiabot_types.ads b/mafiabot_core/src/types/mafiabot_types.ads index b7c4302..4ebbe3c 100644 --- a/mafiabot_core/src/types/mafiabot_types.ads +++ b/mafiabot_core/src/types/mafiabot_types.ads @@ -1,50 +1,15 @@ --- Shared type definitions for the Gen.03 organ-systems body. --- All downstream packages with Mafiabot_Types. +-- Border (D1) shared types. Ada here is the GATE only: it screens messages +-- crossing toward the Brain. It deliberately does NOT model organs (those are +-- R / Octave / Pony / Guile), the inference cycle (cognition), or drive/affect +-- math (the organs' domain, done in floats). The gate needs exactly three +-- things: a source/trust tag, a status code, and a bounded payload to scan. 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; - -- Pin 'Small to 0.01 so the bounds are +/-100 units (fits a byte) rather - -- than GNAT's default 2**-7 small, which would place 1.0 at exactly 128 -- - -- one past a signed-8-bit base range and rejected as "high bound outside - -- type range". - for Axis_Value'Small use 0.01; - - -- Provenance tags — trust boundary uses these to block reclassification + -- Source / trust tag. The border screens by this: external-origin content + -- is never trusted; System_Internal bypasses the blocklist. A message may + -- not reclassify its own provenance (see Trust_Boundary.Validate_Provenance). type Provenance_Tag is ( User_Input, System_Internal, @@ -54,8 +19,30 @@ is Config_Static ); - -- Helpers + -- Return status (replaces exceptions under the No_Exceptions profile). + type Operation_Status is ( + OK, + Error_Invalid_State, + Error_Overflow, + Error_Underflow, + Error_Blocked, -- screened out: injection pattern hit + Error_Trust_Violation, -- provenance reclassification attempt + Error_Config + ); + -- Payload buffer. By the time content reaches the border it has already + -- been pre-digested upstream into bounded RAG context, so a stack-bounded + -- buffer is the right shape: the gate scans it for prompt-injection + -- patterns, it does not stream raw input. 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; + + -- Helpers function Make_Text (S : String) return Bounded_Text with Pre => S'Length <= Max_Text_Length; diff --git a/mafiabot_core/tests/cycle_tests.adb b/mafiabot_core/tests/cycle_tests.adb deleted file mode 100644 index 4eb9ed0..0000000 --- a/mafiabot_core/tests/cycle_tests.adb +++ /dev/null @@ -1,96 +0,0 @@ -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; diff --git a/mafiabot_core/tests/soul_tests.adb b/mafiabot_core/tests/soul_tests.adb deleted file mode 100644 index ce4e145..0000000 --- a/mafiabot_core/tests/soul_tests.adb +++ /dev/null @@ -1,70 +0,0 @@ -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; - -use type Soul.Tarot.Slot_State; - -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; diff --git a/mafiabot_core/tests/trust_tests.adb b/mafiabot_core/tests/trust_tests.adb index e7d03a4..e47ab3a 100644 --- a/mafiabot_core/tests/trust_tests.adb +++ b/mafiabot_core/tests/trust_tests.adb @@ -37,11 +37,9 @@ begin -- 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")); + M : constant Trust_Boundary.Border_Message := + (Provenance => System_Internal, + Payload => Make_Text ("execute")); R : Operation_Status; begin Trust_Boundary.Check_Message (M, R);