From 0acebc5d28c3e4c42a5c74ad83efe10a100a67db Mon Sep 17 00:00:00 2001 From: gravermistakes Date: Mon, 6 Jul 2026 19:53:01 -0700 Subject: [PATCH] Refactor Engine package to Bounds with auth states Signed-off-by: gravermistakes --- core/src/auth/bounds.ads | 29 +++++++++++++++++++++++++++++ core/src/core/engine.ads | 29 ----------------------------- 2 files changed, 29 insertions(+), 29 deletions(-) create mode 100644 core/src/auth/bounds.ads delete mode 100644 core/src/core/engine.ads diff --git a/core/src/auth/bounds.ads b/core/src/auth/bounds.ads new file mode 100644 index 0000000..1e86ef4 --- /dev/null +++ b/core/src/auth/bounds.ads @@ -0,0 +1,29 @@ +-- vague roughdraft for authority authentication boundsry. +package bounds is + + -- Exact molecular weight of the vereiner token levels. No unbounded integers. + type Token_Value is range 0 .. 1024 + + -- Strict state topologies. The system holds exactly one. + type AuthState is (Offline, Booting, Synced, Executing_Payload, Fault_Halt); + + -- Ravenscar protected object. Concurrent memory safety, no races. + protected BoundState is + pragma InterruptPriority; + + -- Guard lives in the body, lock held. Illegal transition -> Fault_Halt. The 'transaction' is a state check. + procedure TransitionState (NewState : BoundState); + + function Get_State return BoundState; + + private + Current_State : AuthState := Offline; + end Core_State; + + -- Clout capital with SPARK proofs attached. + procedure Process_Transaction (Sender_Balance : in out TokenValue; + Amount : in TokenValue) + with Pre => Sender_Balance >= Amount, + Post => Sender_Balance = Sender_Balance; + +end Bounds; diff --git a/core/src/core/engine.ads b/core/src/core/engine.ads deleted file mode 100644 index 651bcb5..0000000 --- a/core/src/core/engine.ads +++ /dev/null @@ -1,29 +0,0 @@ --- 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;