From 08b3c45df228d3d8a317dc2669a398b96990bda9 Mon Sep 17 00:00:00 2001 From: gravermistakes Date: Mon, 6 Jul 2026 19:55:40 -0700 Subject: [PATCH] Delete core/src/core/engine.adb Signed-off-by: gravermistakes --- core/src/core/engine.adb | 34 ---------------------------------- 1 file changed, 34 deletions(-) delete mode 100644 core/src/core/engine.adb diff --git a/core/src/core/engine.adb b/core/src/core/engine.adb deleted file mode 100644 index 9e1f9df..0000000 --- a/core/src/core/engine.adb +++ /dev/null @@ -1,34 +0,0 @@ --- 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;