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

ada: cut to a border-only gate; delete the wrong organ/cognition modeling

Browse Source 
Ada is the D1 border, not the body. Removed everything that pretended otherwise
and completed the real gate so it builds, links, and passes its tests.

Deleted (wrong/defunct/superseded):
- ada_medium.adb (defunct medium, header commented 'WRONG'; replaced by Ichor)
- sockets.{ads,adb} (empty package with an illegal body)
- bbb-bludbrenburier.ads ('this is filler'); invariants-architecture.cobol ('idk cobol')
- tests/soul_tests.adb, tests/cycle_tests.adb (exercise a Soul.Tarot/State/Ada_Medium
  subsystem that does not exist -- the old 56-card/Big-3 design, superseded)

mafiabot_types -> border-only: organs aren't Ada (organs are R/Octave/Pony/Guile),
so drop Organ_Id; drop Cycle_Step (cognition) and the fixed-point Drive/Ratio/
Cost/Axis numerics (drive/affect math lives in the organs, in floats). Keep the
source/trust tag (Provenance_Tag), Operation_Status, and a bounded payload --
content is pre-digested into RAG context upstream, so the gate scans a bounded
buffer for prompt-injection rather than streaming raw input.

trust_boundary: Organ_Message -> Border_Message {Provenance, Payload} (Ada does
not route by organ -- that's Ichor); add the D1 body (blocklist scan, provenance,
rate limit, Trust_Guard) -- the unit Ichor's barrier FFI targets.
Add mafiabot_types.adb. Fix mafiabot_core.gpr (drop phantom dirs + nonexistent
mafiabot.adb main). alire.toml: drop unused gnat_sockets/spark_lemmas.

Builds clean on GNAT 13.3/Alire; trust + config tests pass.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015hmgREHNsxYCuim33yUF2c
This commit is contained in:
Claude
2026-06-18 14:58:27 +00:00
parent b82e4e9833
commit 2a2b698fb4
14 changed files with 207 additions and 589 deletions
Download Patch File Download Diff File Expand all files Collapse all files
mafiabot_core/alire.toml
+3 -3
View File
@@ -8,9 +8,9 @@ maintainers-logins = ["sybad"]
# here, and neither "Proprietary TBD" nor a LicenseRef- custom id is accepted by # 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. # the pinned Alire, so the (optional) field is left out until a license is chosen.
[[depends-on]] # No external crate deps: nothing here `with`s GNAT.Sockets or SPARK.Lemmas.
gnat_sockets = "^1.0.0" # (They were declared for the deleted sockets stub and never used.) Re-add as
spark_lemmas = "^1.0.0" # real needs appear.
# Build modes wildcard "*". Restrictions are NOT a build-switch: see gnat.adc. # Build modes wildcard "*". Restrictions are NOT a build-switch: see gnat.adc.
[build-switches] [build-switches]
mafiabot_core/mafiabot_core.gpr
+9 -12
View File
@@ -2,28 +2,25 @@ with "config/mafiabot_core_config.gpr";
project Mafiabot_Core is 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 for Source_Dirs use
("src", ("src/core",
"src/core",
"src/daemons",
"src/network",
"src/payloads",
"src/types",
"src/config_loader", "src/config_loader",
"src/trust", "src/trust",
"src/organs/soul",
"src/organs/ada_medium",
"src/protocol", "src/protocol",
"src/types",
"config", "config",
"tests"); "tests");
for Object_Dir use "obj"; for Object_Dir use "obj";
for Exec_Dir use "bin"; 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 for Main use
("mafiabot.adb", ("engine_tests.adb",
"engine_tests.adb",
"soul_tests.adb",
"trust_tests.adb", "trust_tests.adb",
"cycle_tests.adb",
"config_tests.adb"); "config_tests.adb");
package Builder is package Builder is
mafiabot_core/src/network/sockets.adb
-2
View File
@@ -1,2 +0,0 @@
package body Sockets is
end Sockets;
mafiabot_core/src/network/sockets.ads
-2
View File
@@ -1,2 +0,0 @@
package Sockets is
end Sockets;
mafiabot_core/src/organs/ada_medium/ada_medium.adb
-344
View File
@@ -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;
mafiabot_core/src/organs/soul/bbb-bludbrenburier.ads
-1
View File
@@ -1 +0,0 @@
-- this is filler
mafiabot_core/src/trust/invariants-architecture.cobol
-1
View File
@@ -1 +0,0 @@
idk cobol
mafiabot_core/src/trust/trust_boundary.adb
+131
View File
@@ -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;
mafiabot_core/src/trust/trust_boundary.ads
+7 -7
View File
@@ -7,10 +7,10 @@ package Trust_Boundary
with SPARK_Mode => On with SPARK_Mode => On
is is
-- Inter-organ message (same type used by Ada_Medium routing) -- A message crossing the border (D1). Ada does not route by organ -- that
type Organ_Message is record -- is Ichor's job -- so this carries only the source/trust tag the gate
Source : Organ_Id := Ada_Medium; -- screens by, plus the (pre-digested) payload to scan.
Destination : Organ_Id := Ada_Medium; type Border_Message is record
Provenance : Provenance_Tag := System_Internal; Provenance : Provenance_Tag := System_Internal;
Payload : Bounded_Text; Payload : Bounded_Text;
end record; end record;
@@ -68,7 +68,7 @@ is
-- Message check (combines provenance + blocklist) -- Message check (combines provenance + blocklist)
procedure Check_Message procedure Check_Message
(Msg : in Organ_Message; (Msg : in Border_Message;
Result : out Operation_Status) Result : out Operation_Status)
with Post => (if Msg.Provenance = System_Internal then Result = OK); with Post => (if Msg.Provenance = System_Internal then Result = OK);
@@ -79,11 +79,11 @@ is
pragma Priority (System.Priority'Last); pragma Priority (System.Priority'Last);
procedure Screen_Inbound procedure Screen_Inbound
(Msg : in Organ_Message; (Msg : in Border_Message;
Status : out Operation_Status); Status : out Operation_Status);
procedure Screen_Outbound procedure Screen_Outbound
(Msg : in Organ_Message; (Msg : in Border_Message;
Status : out Operation_Status); Status : out Operation_Status);
private private
mafiabot_core/src/types/mafiabot_types.adb
+21
View File
@@ -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;
mafiabot_core/src/types/mafiabot_types.ads
+31 -44
View File
@@ -1,50 +1,15 @@
-- Shared type definitions for the Gen.03 organ-systems body. -- Border (D1) shared types. Ada here is the GATE only: it screens messages
-- All downstream packages with Mafiabot_Types. -- 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 package Mafiabot_Types
with SPARK_Mode => On with SPARK_Mode => On
is is
-- Organ identification -- Source / trust tag. The border screens by this: external-origin content
type Organ_Id is (Ada_Medium, Drive_Box, Soul_Organ, Mini_Rag, LLM_Cycle, -- is never trusted; System_Internal bypasses the blocklist. A message may
Trust_Layer, Protocol_Layer); -- not reclassify its own provenance (see Trust_Boundary.Validate_Provenance).
-- 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
type Provenance_Tag is ( type Provenance_Tag is (
User_Input, User_Input,
System_Internal, System_Internal,
@@ -54,8 +19,30 @@ is
Config_Static 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 function Make_Text (S : String) return Bounded_Text
with Pre => S'Length <= Max_Text_Length; with Pre => S'Length <= Max_Text_Length;
mafiabot_core/tests/cycle_tests.adb
-96
View File
@@ -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;
mafiabot_core/tests/soul_tests.adb
-70
View File
@@ -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;
mafiabot_core/tests/trust_tests.adb
+2 -4
View File
@@ -37,10 +37,8 @@ begin
-- System-internal messages always pass Check_Message (proven invariant). -- System-internal messages always pass Check_Message (proven invariant).
declare declare
M : constant Trust_Boundary.Organ_Message := M : constant Trust_Boundary.Border_Message :=
(Source => Ada_Medium, (Provenance => System_Internal,
Destination => Soul_Organ,
Provenance => System_Internal,
Payload => Make_Text ("execute")); Payload => Make_Text ("execute"));
R : Operation_Status; R : Operation_Status;
begin begin