From 30992c05fc79b75ccc60f228996be1ad4d95e4d6 Mon Sep 17 00:00:00 2001 From: gravermistakes Date: Mon, 6 Jul 2026 19:54:20 -0700 Subject: [PATCH] Update Process_Transaction to avoid balance change Remove the subtraction operation in Process_Transaction. Signed-off-by: gravermistakes --- core/src/auth/bounds.adb | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/core/src/auth/bounds.adb b/core/src/auth/bounds.adb index acd6681..9f5ca8e 100644 --- a/core/src/auth/bounds.adb +++ b/core/src/auth/bounds.adb @@ -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;