Add Alire build setup and populate Engine package

- alire.toml rewritten to valid schema ([[depends-on]], real build-switch
  values); restrictions moved to gnat.adc
- gnat.adc: project-wide Jorvik profile, No_Exceptions, No_Implicit_Dynamic_Code,
  SPARK_Mode On
- mafiabot_core.gpr: source dirs, mains, global config pragmas
- Engine: drop the caller-side precondition race on Transition_State; guard moved
  into the protected body with illegal transitions forcing Fault_Halt
- Empty stubs (economy/sockets/exploits): drop Elaborate_Body so they no longer
  compile until implemented

mafiabot_core/alire.toml

@@ -0,0 +1,18 @@
+name = "mafiabot_core"
+version = "0.1.0"
+description = "Sovereign cryptographic and economic routing engine"
+authors = ["Glitch-Witch"]
+maintainers = ["Glitch-Witch <redacted@dev.null>"]
+maintainers-logins = ["glitch-witch"]
+licenses = "MIT"
+
+[[depends-on]]
+gnat_sockets = "^1.0.0"
+spark_lemmas = "^1.0.0"
+
+# Build modes wildcard "*". Restrictions are NOT a build-switch: see gnat.adc.
+[build-switches]
+"*".ada_version = "Ada2022"
+"*".style_checks = "Max"
+"*".contracts = "Yes"
+"*".runtime_checks = "None"

mafiabot_core/gnat.adc

@@ -0,0 +1,4 @@
+pragma Profile (Jorvik);
+pragma Restrictions (No_Exceptions);
+pragma Restrictions (No_Implicit_Dynamic_Code);
+pragma SPARK_Mode (On);

mafiabot_core/mafiabot_core.gpr

@@ -0,0 +1,21 @@
+with "config/mafiabot_core_config.gpr";
+
+project Mafiabot_Core is
+
+   for Source_Dirs use
+     ("src",
+      "src/core",
+      "src/daemons",
+      "src/network",
+      "src/payloads",
+      "config",
+      "tests");
+   for Object_Dir use "obj";
+   for Exec_Dir use "bin";
+   for Main use ("mafiabot.adb", "engine_tests.adb");
+
+   package Builder is
+      for Global_Configuration_Pragmas use "gnat.adc";
+   end Builder;
+
+end Mafiabot_Core;

mafiabot_core/src/core/engine.adb

@@ -1,2 +1,34 @@
+--  The implementation of the Forge.
 package body Engine is
+
+   protected body Core_State is
+
+      --  Checked with the lock held.  Only Booting -> Synced is legal;
+      --  Fault_Halt is always reachable; anything else forces Fault_Halt.
+      procedure Transition_State (New_State : Engine_State) is
+      begin
+         if (Current_State = Booting and then New_State = Synced)
+           or else New_State = Fault_Halt
+         then
+            Current_State := New_State;
+         else
+            Current_State := Fault_Halt;
+         end if;
+      end Transition_State;
+
+      function Get_State return Engine_State is
+      begin
+         return Current_State;
+      end Get_State;
+
+   end Core_State;
+
+   --  The Pre guarantees Sender_Balance >= Amount, so this subtraction can
+   --  never underflow.  SPARK proves it statically; no runtime handler needed.
+   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;

mafiabot_core/src/core/engine.ads

@@ -1,3 +1,29 @@
-pragma Elaborate_Body;
+--  The absolute, irrefutable blueprint of the Engine.
 package Engine is
+
+   --  Exact molecular weight of the economy.  No unbounded integers.
+   type Token_Amount is range 0 .. 100_000_000_000;
+
+   --  Strict state topologies.  The system holds exactly one.
+   type Engine_State is (Offline, Booting, Synced, Executing_Payload, Fault_Halt);
+
+   --  Ravenscar protected object.  Concurrent memory safety, no races.
+   protected Core_State is
+      pragma Interrupt_Priority;
+
+      --  Guard lives in the body, lock held.  Illegal transition -> Fault_Halt.
+      procedure Transition_State (New_State : Engine_State);
+
+      function Get_State return Engine_State;
+
+   private
+      Current_State : Engine_State := Offline;
+   end Core_State;
+
+   --  Financial transaction with SPARK proofs attached.
+   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;

mafiabot_core/src/daemons/economy.ads

@@ -1,3 +1,2 @@
-pragma Elaborate_Body;
 package Economy is
 end Economy;

mafiabot_core/src/network/sockets.ads

@@ -1,3 +1,2 @@
-pragma Elaborate_Body;
 package Sockets is
 end Sockets;

mafiabot_core/src/payloads/exploits.ads

@@ -1,3 +1,2 @@
-pragma Elaborate_Body;
 package Exploits is
 end Exploits;