From 3918ed1c1a9a6b7c788eda05021b6a98000b7bdd Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 31 May 2026 00:25:30 +0000 Subject: [PATCH] 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 | 18 ++++++++++++++ mafiabot_core/gnat.adc | 4 ++++ mafiabot_core/mafiabot_core.gpr | 21 ++++++++++++++++ mafiabot_core/src/core/engine.adb | 32 +++++++++++++++++++++++++ mafiabot_core/src/core/engine.ads | 28 +++++++++++++++++++++- mafiabot_core/src/daemons/economy.ads | 1 - mafiabot_core/src/network/sockets.ads | 1 - mafiabot_core/src/payloads/exploits.ads | 1 - 8 files changed, 102 insertions(+), 4 deletions(-) create mode 100644 mafiabot_core/alire.toml create mode 100644 mafiabot_core/gnat.adc create mode 100644 mafiabot_core/mafiabot_core.gpr diff --git a/mafiabot_core/alire.toml b/mafiabot_core/alire.toml new file mode 100644 index 0000000..840a5a0 --- /dev/null +++ b/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 "] +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" diff --git a/mafiabot_core/gnat.adc b/mafiabot_core/gnat.adc new file mode 100644 index 0000000..e9c0c54 --- /dev/null +++ b/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); diff --git a/mafiabot_core/mafiabot_core.gpr b/mafiabot_core/mafiabot_core.gpr new file mode 100644 index 0000000..cd47e3b --- /dev/null +++ b/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; diff --git a/mafiabot_core/src/core/engine.adb b/mafiabot_core/src/core/engine.adb index d974ae1..9e1f9df 100644 --- a/mafiabot_core/src/core/engine.adb +++ b/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; diff --git a/mafiabot_core/src/core/engine.ads b/mafiabot_core/src/core/engine.ads index 39430e0..651bcb5 100644 --- a/mafiabot_core/src/core/engine.ads +++ b/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; diff --git a/mafiabot_core/src/daemons/economy.ads b/mafiabot_core/src/daemons/economy.ads index 314a20b..0043285 100644 --- a/mafiabot_core/src/daemons/economy.ads +++ b/mafiabot_core/src/daemons/economy.ads @@ -1,3 +1,2 @@ -pragma Elaborate_Body; package Economy is end Economy; diff --git a/mafiabot_core/src/network/sockets.ads b/mafiabot_core/src/network/sockets.ads index 41c88ca..b8557a7 100644 --- a/mafiabot_core/src/network/sockets.ads +++ b/mafiabot_core/src/network/sockets.ads @@ -1,3 +1,2 @@ -pragma Elaborate_Body; package Sockets is end Sockets; diff --git a/mafiabot_core/src/payloads/exploits.ads b/mafiabot_core/src/payloads/exploits.ads index 4f19c16..385a0d7 100644 --- a/mafiabot_core/src/payloads/exploits.ads +++ b/mafiabot_core/src/payloads/exploits.ads @@ -1,3 +1,2 @@ -pragma Elaborate_Body; package Exploits is end Exploits;