Fix: Move mafiabot files from subdirectory to repository root

Reorganize mafiabot source files from nested mafiabot_core/ subdirectory
to root-level structure to match the original file layout. This includes:
- src/: Core Ada source files (engine, daemons, network, payloads)
- config/: Bot configuration modules
- tests/: Test suites

The incorrect subdirectory structure has been removed and replaced with
the proper root-level organization.

config/bot_config.adb

@@ -0,0 +1,4 @@
+pragma SPARK_Mode (Off);
+
+package body Bot_Config is
+end Bot_Config;

config/bot_config.ads

@@ -0,0 +1,28 @@
+--  I/O-facing package: SPARK_Mode Off.
+--  Environment reads are external state; prove the callers, not the reader.
+pragma SPARK_Mode (Off);
+
+package Bot_Config is
+
+   Config_Missing : exception;
+
+   Max_Token_Length : constant := 256;
+   Max_Guild_Length : constant := 64;
+
+   subtype Token_Buffer is String (1 .. Max_Token_Length);
+   subtype Guild_Buffer is String (1 .. Max_Guild_Length);
+
+   type Bot_Configuration is record
+      Bot_Token       : Token_Buffer := (others => ' ');
+      Token_Length    : Natural      := 0;
+      Guild_ID        : Guild_Buffer := (others => ' ');
+      Guild_Length    : Natural      := 0;
+      Command_Prefix  : Character   := '!';
+      Max_Connections : Positive    := 4;
+      Request_Timeout : Duration    := 30.0;
+   end record;
+
+   function  Load     return Bot_Configuration;
+   procedure Validate (Config : Bot_Configuration);
+
+end Bot_Config;

src/core/engine.adb

@@ -0,0 +1,42 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (On);
+
+package body Engine is
+
+   protected body Core_State is
+
+      procedure Transition_State (New_State : Engine_State) is
+      begin
+         Current_State := New_State;
+      end Transition_State;
+
+      function Get_State return Engine_State is
+      begin
+         return Current_State;
+      end Get_State;
+
+   end Core_State;
+
+   procedure Initialize (Registry : out Daemon_Registry) is
+   begin
+      Registry := (others => Stopped);
+   end Initialize;
+
+   procedure Start_Daemon (Registry : in out Daemon_Registry; D : Daemon_Kind) is
+   begin
+      Registry (D) := Running;
+   end Start_Daemon;
+
+   procedure Stop_Daemon (Registry : in out Daemon_Registry; D : Daemon_Kind) is
+   begin
+      Registry (D) := Stopped;
+   end Stop_Daemon;
+
+   procedure Process_Transaction
+     (Sender_Balance : in out Token_Amount;
+      Amount         : in     Token_Amount) is
+   begin
+      Sender_Balance := Sender_Balance - Amount;
+   end Process_Transaction;
+
+end Engine;

src/core/engine.ads

@@ -0,0 +1,61 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (On);
+
+--  The Forge. Mathematically proven. Statically verified.
+--  If the SPARK prover does not sign off, the binary does not exist.
+package Engine is
+
+   --  Exact integer units. No floating-point. No rounding surprises.
+   type Token_Amount is range 0 .. 100_000_000_000
+     with Size => 64;
+
+   --  The only legal topologies of the engine.
+   type Engine_State is
+     (Offline, Booting, Synced, Executing_Payload, Fault_Halt);
+
+   --  Ravenscar protected object: the compiler physically rejects race conditions.
+   protected Core_State is
+      pragma Interrupt_Priority;
+
+      --  Only Booting -> Synced or anything -> Fault_Halt are legal transitions.
+      procedure Transition_State (New_State : Engine_State)
+        with Pre => (Get_State = Booting and then New_State = Synced)
+                    or else New_State = Fault_Halt;
+
+      function Get_State return Engine_State;
+
+   private
+      Current_State : Engine_State := Offline;
+   end Core_State;
+
+   --  Daemon orchestration layer.
+   type Daemon_Kind  is (Economy_Daemon, Network_Daemon, Exploit_Daemon);
+   type Daemon_State is (Stopped, Running, Faulted);
+   type Daemon_Registry is array (Daemon_Kind) of Daemon_State;
+
+   procedure Initialize (Registry : out Daemon_Registry)
+     with Post => (for all D in Daemon_Kind => Registry (D) = Stopped);
+
+   procedure Start_Daemon (Registry : in out Daemon_Registry; D : Daemon_Kind)
+     with Pre  => Registry (D) = Stopped,
+          Post => Registry (D) = Running
+                  and then
+                  (for all Other in Daemon_Kind =>
+                     (if Other /= D then Registry (Other) = Registry'Old (Other)));
+
+   procedure Stop_Daemon (Registry : in out Daemon_Registry; D : Daemon_Kind)
+     with Pre  => Registry (D) = Running,
+          Post => Registry (D) = Stopped
+                  and then
+                  (for all Other in Daemon_Kind =>
+                     (if Other /= D then Registry (Other) = Registry'Old (Other)));
+
+   --  The crown jewel: a transaction that cannot underflow.
+   --  The SPARK prover will reject any call site that cannot guarantee Sender >= Amount.
+   procedure Process_Transaction
+     (Sender_Balance : in out Token_Amount;
+      Amount         : in     Token_Amount)
+     with Pre  => Sender_Balance >= Amount,
+          Post => Sender_Balance = Sender_Balance'Old - Amount;
+
+end Engine;

src/daemons/economy.adb

@@ -0,0 +1,5 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (On);
+
+package body Economy is
+end Economy;

src/daemons/economy.ads

@@ -0,0 +1,62 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (On);
+
+--  The casino math daemon. Fixed-point decimal. No Float. Ever.
+package Economy is
+
+   --  One hundred billion units max. delta 0.01 for cent-precision.
+   type Token_Amount is delta 0.01 range 0.00 .. 1_000_000_000.00
+     with Small => 0.01;
+
+   type Player_ID is new Positive range 1 .. 10_000;
+
+   type Balance_Entry is record
+      ID      : Player_ID;
+      Balance : Token_Amount := 0.00;
+      Wagered : Token_Amount := 0.00;
+   end record;
+
+   Max_Entries : constant := 10_000;
+   type Ledger_Index is range 1 .. Max_Entries;
+   type Ledger_Array is array (Ledger_Index) of Balance_Entry;
+
+   type Ledger is record
+      Entries : Ledger_Array;
+      Count   : Natural := 0;
+   end record
+     with Predicate => Ledger.Count <= Max_Entries;
+
+   Insufficient_Funds : exception;
+   Player_Not_Found   : exception;
+
+   procedure Register (L : in out Ledger; ID : Player_ID)
+     with Pre  => L.Count < Max_Entries,
+          Post => L.Count = L.Count'Old + 1;
+
+   function Balance_Of (L : Ledger; ID : Player_ID) return Token_Amount
+     with Pre => (for some I in Ledger_Index range 1 .. Ledger_Index (L.Count) =>
+                    L.Entries (I).ID = ID);
+
+   procedure Deposit
+     (L      : in out Ledger;
+      ID     : Player_ID;
+      Amount : Token_Amount)
+     with Pre => (for some I in Ledger_Index range 1 .. Ledger_Index (L.Count) =>
+                    L.Entries (I).ID = ID);
+
+   procedure Place_Wager
+     (L      : in out Ledger;
+      ID     : Player_ID;
+      Amount : Token_Amount)
+     with Pre => (for some I in Ledger_Index range 1 .. Ledger_Index (L.Count) =>
+                    L.Entries (I).ID = ID
+                    and then L.Entries (I).Balance >= Amount);
+
+   procedure Resolve_Wager
+     (L   : in out Ledger;
+      ID  : Player_ID;
+      Won : Boolean)
+     with Pre => (for some I in Ledger_Index range 1 .. Ledger_Index (L.Count) =>
+                    L.Entries (I).ID = ID);
+
+end Economy;

src/mafiabot.adb

@@ -0,0 +1,12 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (Off);  --  Main procedure: orchestrates I/O-facing init.
+
+with Bot_Config;
+with Engine;
+
+procedure Mafiabot is
+   Config   : Bot_Config.Bot_Configuration;
+   Registry : Engine.Daemon_Registry;
+begin
+   null;
+end Mafiabot;

src/network/sockets.adb

@@ -0,0 +1,4 @@
+pragma SPARK_Mode (Off);
+
+package body Sockets is
+end Sockets;

src/network/sockets.ads

@@ -0,0 +1,30 @@
+--  External I/O: SPARK_Mode Off.
+--  GNAT.Sockets uses access types; prove the callers via contracts on this boundary.
+pragma SPARK_Mode (Off);
+
+with GNAT.Sockets; use GNAT.Sockets;
+
+package Sockets is
+
+   type Connection is record
+      Sock   : Socket_Type := No_Socket;
+      Port   : Port_Type   := 443;
+      Active : Boolean     := False;
+   end record;
+
+   Connect_Failed  : exception;
+   Send_Failed     : exception;
+   Receive_Failed  : exception;
+
+   procedure Open_Connection
+     (C    : out Connection;
+      Host : String;
+      Port : Port_Type := 443);
+
+   procedure Close_Connection (C : in out Connection);
+
+   procedure Send_Raw    (C : Connection; Data : String);
+   function  Receive_Raw (C : Connection) return String;
+   function  Is_Active   (C : Connection) return Boolean;
+
+end Sockets;

src/payloads/exploits.adb

@@ -0,0 +1,5 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (On);
+
+package body Exploits is
+end Exploits;

src/payloads/exploits.ads

@@ -0,0 +1,90 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (On);
+
+--  Structured payload types for authorized security operations.
+--  The threat actor demands perfectly typed, statically verified dispatch.
+package Exploits is
+
+   type Action_Kind is
+     (Probe,
+      Inject,
+      Exfil,
+      Pivot,
+      Shell,
+      Patch,
+      Abort_Op);
+
+   --  Fixed-size target descriptor. No heap. No surprises.
+   Max_Host_Length  : constant := 253;  --  RFC 1035 max hostname
+   Max_Path_Length  : constant := 2048;
+   Max_Proto_Length : constant := 16;
+
+   subtype Host_Buffer  is String (1 .. Max_Host_Length);
+   subtype Path_Buffer  is String (1 .. Max_Path_Length);
+   subtype Proto_Buffer is String (1 .. Max_Proto_Length);
+
+   type Target_Spec is record
+      Host       : Host_Buffer  := (others => ' ');
+      Host_Len   : Natural      := 0;
+      Port       : Natural      := 0;
+      Path       : Path_Buffer  := (others => ' ');
+      Path_Len   : Natural      := 0;
+      Proto      : Proto_Buffer := (others => ' ');
+      Proto_Len  : Natural      := 0;
+   end record
+     with Predicate =>
+       Target_Spec.Host_Len  <= Max_Host_Length  and then
+       Target_Spec.Path_Len  <= Max_Path_Length  and then
+       Target_Spec.Proto_Len <= Max_Proto_Length;
+
+   Max_Payload_Length : constant := 65_536;
+   subtype Payload_Buffer is String (1 .. Max_Payload_Length);
+
+   type Exploit is record
+      Action      : Action_Kind;
+      Target      : Target_Spec;
+      Op_ID       : Natural := 0;
+      Round       : Natural := 0;
+      Timestamp   : Natural := 0;
+      Payload     : Payload_Buffer := (others => ' ');
+      Payload_Len : Natural        := 0;
+   end record
+     with Predicate => Exploit.Payload_Len <= Max_Payload_Length;
+
+   Invalid_Exploit : exception;
+
+   function Build_Probe
+     (Target : Target_Spec; Op_ID : Natural) return Exploit
+     with Post => Build_Probe'Result.Action = Probe
+                  and then Build_Probe'Result.Op_ID = Op_ID;
+
+   function Build_Inject
+     (Target : Target_Spec; Op_ID : Natural;
+      Data   : String) return Exploit
+     with Pre  => Data'Length <= Max_Payload_Length,
+          Post => Build_Inject'Result.Action = Inject
+                  and then Build_Inject'Result.Payload_Len = Data'Length;
+
+   function Build_Exfil
+     (Target : Target_Spec; Op_ID : Natural) return Exploit
+     with Post => Build_Exfil'Result.Action = Exfil;
+
+   function Build_Pivot
+     (Target : Target_Spec; Op_ID : Natural) return Exploit
+     with Post => Build_Pivot'Result.Action = Pivot;
+
+   function Build_Shell
+     (Target : Target_Spec; Op_ID : Natural;
+      Cmd    : String) return Exploit
+     with Pre  => Cmd'Length <= Max_Payload_Length,
+          Post => Build_Shell'Result.Action = Shell
+                  and then Build_Shell'Result.Payload_Len = Cmd'Length;
+
+   function Build_Abort (Op_ID : Natural) return Exploit
+     with Post => Build_Abort'Result.Action = Abort_Op
+                  and then Build_Abort'Result.Op_ID = Op_ID;
+
+   function Serialize (E : Exploit) return String
+     with Pre => E.Payload_Len <= Max_Payload_Length;
+
+end Exploits;

tests/engine_tests.adb

@@ -0,0 +1,12 @@
+pragma Profile (Jorvik);
+pragma SPARK_Mode (Off);  --  Test harness: Off; prove the units, not the runner.
+
+with Engine;
+with Economy;
+
+procedure Engine_Tests is
+   Registry : Engine.Daemon_Registry;
+begin
+   Engine.Initialize (Registry);
+   pragma Assert (for all D in Engine.Daemon_Kind => Registry (D) = Engine.Stopped);
+end Engine_Tests;