mirror of
https://github.com/SHOGGOTH-SECTOR/sica-fondt.git
synced 2026-09-30 01:15:10 +00:00
Add Gen.03 organ-systems core: Ada Medium, Soul/Tarot, trust boundary, Hermes MCP bridge
Implements the Gen.03 organ-systems body in SPARK/Ada (Jorvik, No_Exceptions): - Shared types (mafiabot_types): Bounded_Text, Operation_Status, Organ_Id, Provenance_Tag, fixed-point drive/ratio/cost/axis types. - Config loader: SPARK-safe flat key-value parser (no heap/exceptions/finalization). - Trust boundary: blocklist substring matching, provenance enforcement, tick-based rate limiting, Trust_Guard protected object. - Soul / Silicon Dawn Tarot: 56-card alphabet, Celtic Cross spread, Big-3 identity anchors. The cross accretes from the cognitive loops (2 cards per layer at steps 6/9/13, stave of 4 at step 17) rather than being drawn whole. - Sessions: Soul_State is now keyed by (uid, channel, server). Each session has its own card pool, cross, and output counter; the Big-3 identity is global. A formed cross is held for the session (or 17 outputs, whichever is longer). Two users on two channels never share a deck or a cross. - Ada Medium: 23-step forward-only inference cycle wiring the cognitive loops, Celtic Cross injection, and outbound trust screening per session. - Hermes MCP stdio bridge: JSON-RPC over stdin/stdout (initialize, tools/list, tools/call), SOUL.md generation, verbatim id echo. SPARK_Mode Off for I/O; trust checks run in proven code first. - Main driver: organ init -> SOUL.md publish -> MCP serve loop. - Tests: soul, trust, cycle (session formation/isolation), config. Fixes an orchestrator bug where step 1 advanced onto Phase_Input after Reset, failing every cycle. Note: requires GNAT/Alire to build; no Ada toolchain in this environment, so compilation and gnatprove must run in CI.
This commit is contained in:
@@ -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;
|
||||
@@ -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;
|
||||
Reference in New Issue
Block a user