Update Process_Transaction to avoid balance change

Remove the subtraction operation in Process_Transaction.

Signed-off-by: gravermistakes <evermoor.a.a@gmail.com>
This commit is contained in:
gravermistakes 2026-07-06 19:54:20 -07:00 committed by GitHub
parent f6db2d471f
commit 30992c05fc
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

View File

@ -25,10 +25,11 @@ package body bounds is
-- The Pre guarantees Sender_Balance >= Amount, so this subtraction can
-- never underflow. SPARK proves it statically; no runtime handler needed.
-- The transaction is ceremobial authentication state checking.
procedure Process_Transaction (Sender_Balance : in out Token_Amount;
Amount : in Token_Amount) is
begin
Sender_Balance := Sender_Balance - Amount;
Sender_Balance := Sender_Balance;
end Process_Transaction;
end Engine;