From 78d8582719cef202deb7992bdd0378b7aedcf39a Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Sun, 31 May 2026 15:33:46 +0000
Subject: [PATCH] evm-semantics/evm.md: rewrite #transferFunds same-account
 rule, move linearity to side condition
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The same-account variant of #transferFunds was

    rule <k> #transferFunds ACCT ACCT VALUE => .K ... </k>
         ...
      requires VALUE <=Int ORIGFROM

i.e. the linearity guard `ACCT ACCT` required the two account-id
arguments to be syntactically identical. Booster's matcher cannot
discharge that on distinct-named symbolic variables (e.g.
`#transferFunds ?CONTRACT_ID 1 0`), even when the path constraint
implies their distinctness — match returns Indeterminate, booster
aborts, and the proof yields to kore.

Reformulate as

    rule <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k>
         ...
      requires ACCTFROM ==K ACCTTO andBool VALUE <=Int ORIGFROM

The LHS now uses distinct variable names so the match is unconditional;
the original linearity moves into the side condition as `==K`, which
booster can discharge via the path constraint (or via its SMT path)
without an indeterminate-match abort. Semantically equivalent on
concrete inputs and strictly more permissive on symbolic inputs in a
sound direction (matches when args are semantically equal but not
syntactically).

Recover-mode sweep identified 12 kore-execute handoffs (all benchmarks
ecrecover variants) caused by this exact match-fail abort. Validated
locally on benchmarks/ecrecover00-siginvalid-spec.k together with the
#asAccount [total] fix in the preceding commit: the spec's recover-mode
kcfg went from 2 kore-handoffs to 0, proof still passes.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
(cherry picked from commit 1bff5e84ed608edeeb5e403e748b342e40f33f4b)
---
 kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
index 27547a6feb..731a432e43 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -1080,13 +1080,14 @@ These are just used by the other operators for shuffling local execution state a
     syntax InternalOp ::= "#transferFunds" Int Int Int
                         | "#transferFundsToNonExistent" Int Int Int
  // ---------------------------------------------------------------
-    rule <k> #transferFunds ACCT ACCT VALUE => .K ... </k>
+    rule <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k>
          <account>
-           <acctID> ACCT </acctID>
+           <acctID> ACCTFROM </acctID>
            <balance> ORIGFROM </balance>
            ...
          </account>
-      requires VALUE <=Int ORIGFROM
+      requires ACCTFROM ==K ACCTTO
+       andBool VALUE <=Int ORIGFROM
 
     rule <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k>
          <account>