diff --git a/config/bot_config.adb b/config/bot_config.adb new file mode 100644 index 0000000..5f99cde --- /dev/null +++ b/config/bot_config.adb @@ -0,0 +1,4 @@ +pragma SPARK_Mode (Off); + +package body Bot_Config is +end Bot_Config; diff --git a/config/bot_config.ads b/config/bot_config.ads new file mode 100644 index 0000000..76f321a --- /dev/null +++ b/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; diff --git a/mafiabot_core/.gitignore b/mafiabot_core/.gitignore deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/alire.toml b/mafiabot_core/alire.toml deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/core/engine.adb b/mafiabot_core/src/core/engine.adb deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/core/engine.ads b/mafiabot_core/src/core/engine.ads deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/daemons/economy.adb b/mafiabot_core/src/daemons/economy.adb deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/daemons/economy.ads b/mafiabot_core/src/daemons/economy.ads deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/mafiabot.adb b/mafiabot_core/src/mafiabot.adb deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/network/sockets.adb b/mafiabot_core/src/network/sockets.adb deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/network/sockets.ads b/mafiabot_core/src/network/sockets.ads deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/payloads/exploits.adb b/mafiabot_core/src/payloads/exploits.adb deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/src/payloads/exploits.ads b/mafiabot_core/src/payloads/exploits.ads deleted file mode 100644 index e69de29..0000000 diff --git a/mafiabot_core/tests/engine_tests.adb b/mafiabot_core/tests/engine_tests.adb deleted file mode 100644 index e69de29..0000000 diff --git a/src/core/engine.adb b/src/core/engine.adb new file mode 100644 index 0000000..41dce39 --- /dev/null +++ b/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; diff --git a/src/core/engine.ads b/src/core/engine.ads new file mode 100644 index 0000000..a9dd53e --- /dev/null +++ b/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; diff --git a/src/daemons/economy.adb b/src/daemons/economy.adb new file mode 100644 index 0000000..f498862 --- /dev/null +++ b/src/daemons/economy.adb @@ -0,0 +1,5 @@ +pragma Profile (Jorvik); +pragma SPARK_Mode (On); + +package body Economy is +end Economy; diff --git a/src/daemons/economy.ads b/src/daemons/economy.ads new file mode 100644 index 0000000..43ee726 --- /dev/null +++ b/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; diff --git a/src/mafiabot.adb b/src/mafiabot.adb new file mode 100644 index 0000000..2cfaf66 --- /dev/null +++ b/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; diff --git a/src/network/sockets.adb b/src/network/sockets.adb new file mode 100644 index 0000000..72fbeef --- /dev/null +++ b/src/network/sockets.adb @@ -0,0 +1,4 @@ +pragma SPARK_Mode (Off); + +package body Sockets is +end Sockets; diff --git a/src/network/sockets.ads b/src/network/sockets.ads new file mode 100644 index 0000000..a967671 --- /dev/null +++ b/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; diff --git a/src/payloads/exploits.adb b/src/payloads/exploits.adb new file mode 100644 index 0000000..ce364c9 --- /dev/null +++ b/src/payloads/exploits.adb @@ -0,0 +1,5 @@ +pragma Profile (Jorvik); +pragma SPARK_Mode (On); + +package body Exploits is +end Exploits; diff --git a/src/payloads/exploits.ads b/src/payloads/exploits.ads new file mode 100644 index 0000000..e52f09f --- /dev/null +++ b/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; diff --git a/tests/engine_tests.adb b/tests/engine_tests.adb new file mode 100644 index 0000000..04fac89 --- /dev/null +++ b/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;