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;