diff --git a/core/src/auth/bounds.ads b/core/src/auth/bounds.ads index 1e86ef4..e1f3848 100644 --- a/core/src/auth/bounds.ads +++ b/core/src/auth/bounds.ads @@ -2,12 +2,12 @@ package bounds is -- Exact molecular weight of the vereiner token levels. No unbounded integers. - type Token_Value is range 0 .. 1024 + type Token_Value is range 0 .. 512 -- 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. + -- JORVIK protected object. Concurrent memory safety, no races. protected BoundState is pragma InterruptPriority; @@ -20,10 +20,6 @@ package bounds is 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; + -- not a thing end Bounds;