include/, kevm-pyk/, tests/specs/: rework/simplify allBut64th logic

Author: ehildenb

include/kframework/evm.md

@@ -2327,8 +2327,7 @@ There are several helpers for calculating gas (most of them also specified in th
 
     syntax Int ::= #allBut64th ( Int ) [function, total, smtlib(gas_allBut64th)]
  // ----------------------------------------------------------------------------
-    rule [allBut64th.pos]: #allBut64th(N) => N -Int (N /Int 64) requires 0 <=Int N
-    rule [allBut64th.neg]: #allBut64th(N) => 0                  requires N  <Int 0
+    rule [allBut64th]: #allBut64th(N) => N -Int (N /Int 64)
 ```
 
 ```{.k .nobytes}

include/kframework/infinite-gas.md

@@ -141,8 +141,8 @@ module INFINITE-GAS-COMMON
     rule         Cextra(_, _, _, _) <Int #gas(_) => true [simplification]
     rule         Cextra(_, _, _, _) <Int pow256  => true [simplification]
 
-    rule 0 <=Int #allBut64th(_)                => true                          [simplification]
-    rule         #allBut64th(G)  <Int #gas(G') => true requires G <Int #gas(G') [simplification]
+    rule 0 <=Int #allBut64th(G)         => true requires 0 <=Int G  [simplification]
+    rule         #allBut64th(G) <Int G' => true requires G  <Int G' [simplification]
 
     rule 0 <=Int _:ScheduleConst < _:Schedule >               => true [simplification]
     rule         _:ScheduleConst < _:Schedule >  <Int #gas(_) => true [simplification]

include/kframework/lemmas/lemmas.k

@@ -27,7 +27,7 @@ module LEMMAS [symbolic]
     rule maxUInt48  &Int X <Int pow48  => true requires 0 <=Int X [simplification, smt-lemma]
     rule maxUInt160 &Int X <Int pow160 => true requires 0 <=Int X [simplification, smt-lemma]
 
-    rule (X /Int 64) +Int #allBut64th(X) => X requires 0 <=Int X [simplification]
+    rule (X /Int 64) +Int #allBut64th(X) => X [simplification]
 
   // ########################
   // Set Reasoning

kevm-pyk/src/kevm_pyk/kevm.py

@@ -121,7 +121,7 @@ def hook_namespaces() -> List[str]:
     @staticmethod
     def concrete_rules() -> List[str]:
         return [
-            'EVM.allBut64th.pos',
+            'EVM.allBut64th',
             'EVM.Caddraccess',
             'EVM.Cbalance.new',
             'EVM.Cbalance.old',

tests/specs/concrete-rules.txt

@@ -1,4 +1,4 @@
-EVM.allBut64th.pos
+EVM.allBut64th
 EVM.Caddraccess
 EVM.Cbalance.new
 EVM.Cbalance.old

tests/specs/functional/infinite-gas-spec.k

@@ -33,8 +33,6 @@ module INFINITE-GAS-SPEC
 
     claim <k> runLemma(((VGas -Int (#allBut64th(VGas +Int -2655) +Int 700)) +Int #allBut64th(VGas +Int -2655)) +Int -7244) => doneLemma(VGas +Int -7944) ... </k>
 
-    claim [allBut64th-1]: <k> runLemma(((VGAS +Int -32247) /Int 64) +Int #allBut64th(VGAS +Int -32247)) => doneLemma(VGAS +Int -32247) ... </k> requires 0 <=Int VGAS
-
     claim <k> runLemma(X +Int (0 -Int ABI_wad)) => doneLemma(X -Int ABI_wad) ... </k>
 
     claim <k> runLemma(#memoryUsageUpdate(#memoryUsageUpdate(MEMORYUSED_CELL, 0, 32), 32, 32)) => doneLemma(#memoryUsageUpdate(MEMORYUSED_CELL, 32, 32)) ... </k>
@@ -56,8 +54,6 @@ module INFINITE-GAS-SPEC
     claim <k> runLemma(#gas(#gas(G1 -Int G2) +Int #allBut64th(G3))) => doneLemma(#gas((G1 -Int G2) +Int #allBut64th(G3))) ... </k> requires 0 <Int G3
     claim <k> runLemma(#gas(#gas(G1 -Int G2) -Int #allBut64th(G3))) => doneLemma(#gas((G1 -Int G2) -Int #allBut64th(G3))) ... </k> requires 0 <Int G3 andBool G3 <Int #gas(G1 -Int G2)
 
-    claim <k> runLemma(#gas(G) +Int (#allBut64th((VGas -Int Csstore(ISTANBUL, V1, V2, V3)) +Int -3232) +Int -3232)) => doneLemma(#gas(G +Int (#allBut64th((VGas -Int Csstore(ISTANBUL, V1, V2, V3)) +Int -3232) +Int -3232))) ... </k>
-    claim <k> runLemma(#gas(G) +Int ((#allBut64th(VGas -Int Csstore(ISTANBUL, V1, V2, V3)) -Int Csstore(ISTANBUL, V1', V2', V3')) +Int -3232)) => doneLemma(#gas(G +Int ((#allBut64th(VGas -Int Csstore(ISTANBUL, V1, V2, V3)) -Int Csstore(ISTANBUL, V1', V2', V3')) +Int -3232))) ... </k>
 
     claim <k> runLemma(#gas(G) -Int Cmem(SCHED, #memoryUsageUpdate(MU, W0, 32))) => doneLemma(#gas(G -Int Cmem(SCHED, #memoryUsageUpdate(MU, W0, 32)))) ... </k>
            requires #rangeUInt(256, MU) andBool #rangeUInt(256, W0)

tests/specs/functional/lemmas-spec.k

@@ -66,6 +66,8 @@ module LEMMAS-SPEC
                                      => doneLemma(368263281805664599098893944405654396525700029268) ... </k>
                                   requires #rangeUInt(256, X)
 
+    claim [allBut64th-1]: <k> runLemma(((VGAS +Int -32247) /Int 64) +Int #allBut64th(VGAS +Int -32247)) => doneLemma(VGAS +Int -32247) ... </k>
+
  // Buffer write simplifications
  // ----------------------------