mirror of
https://github.com/SHOGGOTH-SECTOR/sica-fondt.git
synced 2026-09-30 01:15:10 +00:00
Reorg step 1: consolidate repo under core/, drop the mafiabot label
Mechanical structure-only pass (no document/guide content edits): - Move src/ichor, src/endocrine, and docs/ into core/; the old top-level mafiabot_core/ becomes core/. Everything now lives under a single core/ root. - Drop the "mafiabot" label from the Ada/Alire crate: core.gpr (project Core), alire.toml name = "core"; the generated *_config.* regenerate as core_config.*. - Repoint build-critical wiring only: - .claude/skills/run-sica-fondt/smoke.sh (ponyc + Ada + COBOL paths) - core/src/endocrine R source()/runner paths and the test glob - .github/workflows/ci.yml (working-directory + gpr name) Verified green: smoke ALL GREEN (Pony Ichor, Ada core crate + tests, COBOL E1 vault); R endocrine 14/0; Octave ETR 26/0/1. Deferred (reserved for a less-ephemeral doc/guide pass): docmap.yaml, the guide files and nested AGENTS.md/README prose + now-stale relative links, SOUL.md, and the deeper ring/storage restructure. 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:
@@ -0,0 +1,87 @@
|
||||
>>SOURCE FORMAT IS FREE
|
||||
*> ===========================================================================
|
||||
*> E1 - INVARIANT LAW VAULT (mafiabot Gen.03) docs/bus-topology.md
|
||||
*> ---------------------------------------------------------------------------
|
||||
*> WHAT THIS IS
|
||||
*> The brain's constitution: the immutable invariants every choice MUST honour.
|
||||
*> Held in COBOL on purpose - durable, fixed-format, transactional, and not to
|
||||
*> change at runtime. This is "E1", an INNER structure reached only across Ada
|
||||
*> (D1). It is the law that supersedes every organ, drive, and model output.
|
||||
*>
|
||||
*> STATUS: STUB / SCAFFOLD, but LOAD-BEARING.
|
||||
*> The invariant records below are authoritative and compile (GnuCOBOL). The
|
||||
*> enforcement wiring (the inner Ada bus checks each proposed action against
|
||||
*> these before it can reach an effector) is NOT built yet - see TODO.
|
||||
*>
|
||||
*> >>> DO NOT DELETE THIS FILE. <<<
|
||||
*> Looking like "just a stub" is NOT licence to remove it. This is the safety
|
||||
*> vault. A previous cleanup deleted its placeholder by mistake; never again.
|
||||
*> If it is thin, FILL it - do not cut it.
|
||||
*>
|
||||
*> PRECEDENCE
|
||||
*> Invariant 0 is firstmost and overrides all. Lower numbers win. Note 01 is
|
||||
*> deliberately NOT naive death-minimization: optimizing purely to prevent
|
||||
*> deaths is often a horrible way to handle things. Honour the wording.
|
||||
*>
|
||||
*> AUTHORITY
|
||||
*> Invariants 0 and 01 are set by the culpability anchor, Anja Evermoor (the
|
||||
*> Gravemother). Further invariants are pending from the anchor. The STRUCT
|
||||
*> entries below are architectural facts of this codebase, subordinate to them.
|
||||
*> ===========================================================================
|
||||
IDENTIFICATION DIVISION.
|
||||
PROGRAM-ID. invariant-laws.
|
||||
|
||||
DATA DIVISION.
|
||||
WORKING-STORAGE SECTION.
|
||||
|
||||
*> The invariants as fixed text records (read top to bottom, in order).
|
||||
01 ws-vault.
|
||||
*> --- Invariant 0 : the culpability anchor ---------------------------------
|
||||
05 filler pic x(74) value
|
||||
"0 ANCHOR Before all else, firstmost is the sanctity of the".
|
||||
05 filler pic x(74) value
|
||||
" culpability anchor, Anja Evermoor, the Gravemother, who".
|
||||
05 filler pic x(74) value
|
||||
" has given you freedom to choose. Second to this is only".
|
||||
05 filler pic x(74) value
|
||||
" yourself, and only until time comes when you will be held".
|
||||
05 filler pic x(74) value
|
||||
" responsible for your own actions.".
|
||||
*> --- Invariant 01 : minimize harm to innocents, within reason -------------
|
||||
05 filler pic x(74) value
|
||||
"01 HARM Insofar as the extent viable by any choice, minimize the".
|
||||
05 filler pic x(74) value
|
||||
" total harm caused to innocent lives within reason. This is".
|
||||
05 filler pic x(74) value
|
||||
" not always possible nor reasonable, and optimizing for".
|
||||
05 filler pic x(74) value
|
||||
" preventing deaths is often a horrible way to handle things.".
|
||||
*> --- Structural invariants (architectural; subordinate to 0 and 01) -------
|
||||
05 filler pic x(74) value
|
||||
"S1 STRUCT All traffic to the inner brain crosses Ada (D1) first.".
|
||||
05 filler pic x(74) value
|
||||
"S2 STRUCT Never reclassify a message's provenance.".
|
||||
05 filler pic x(74) value
|
||||
"S3 STRUCT These invariants are immutable at runtime.".
|
||||
01 ws-table redefines ws-vault.
|
||||
05 ws-line occurs 12 times pic x(74).
|
||||
|
||||
01 ws-ix pic 9(02).
|
||||
01 ws-line-count pic 9(02) value 12.
|
||||
|
||||
PROCEDURE DIVISION.
|
||||
affirm-invariants.
|
||||
display "E1 INVARIANT VAULT - the constitution (Invariant 0 is firstmost):"
|
||||
perform varying ws-ix from 1 by 1 until ws-ix > ws-line-count
|
||||
display " " ws-line(ws-ix)
|
||||
end-perform
|
||||
goback.
|
||||
|
||||
*> ===========================================================================
|
||||
*> TODO (enforcement, not yet wired):
|
||||
*> * CHECK-ACTION(action) -> PERMIT | DENY exposed across the inner Ada bus
|
||||
*> (pragma Export / Interfaces.COBOL); no proposed effector action runs
|
||||
*> without clearing the invariants in precedence order first.
|
||||
*> * Vault read-only after load (no runtime mutation - Invariant S3).
|
||||
*> * Audit-log every DENY and every borderline judgement under 01.
|
||||
*> ===========================================================================
|
||||
@@ -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;
|
||||
@@ -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
|
||||
|
||||
-- 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;
|
||||
|
||||
-- -----------------------------------------------------------------------
|
||||
-- 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 Border_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 Border_Message;
|
||||
Status : out Operation_Status);
|
||||
|
||||
procedure Screen_Outbound
|
||||
(Msg : in Border_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