mirror of
https://github.com/SHOGGOTH-SECTOR/sica-fondt.git
synced 2026-07-31 08:06:26 +00:00
Delete core/src/core/engine.adb
Signed-off-by: gravermistakes <evermoor.a.a@gmail.com>
This commit is contained in:
parent
0acebc5d28
commit
08b3c45df2
@ -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;
|
||||
Loading…
x
Reference in New Issue
Block a user