Additional EVM optimizations

src/kontrol/cli.py

@@ -357,6 +357,13 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Include auxiliary Kontrol lemmas.',
     )
+    build.add_argument(
+        '--evm-rule-optimizations',
+        dest='evm_rule_optimizations',
+        default=None,
+        action='store_true',
+        help='Optimize KEVM execution. Assumes running Solidity-compiled bytecode cannot result in a stack overflow/underflow.',
+    )
 
     state_diff_args = command_parser.add_parser(
         'load-state',

src/kontrol/kdist/evm_rule_optimizations.md

@@ -0,0 +1,114 @@
+Highly optimized EVM rules
+==========================
+
+The provided rules speed up execution and rely on the hypothesis that EVM bytecode
+that comes compiled from Solidity will not result in word stack overflows or underflows.
+
+```k
+module EVM-RULE-OPTIMIZATIONS
+    imports EVM
+
+    rule #stackUnderflow(_, _) => false [priority(30)]
+    rule #stackOverflow(_, _) => false [priority(30)]
+
+    rule [super.optimized.pushzero]:
+      <k> ( #next[ PUSHZERO ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> WS => 0 : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.push]:
+      <k> ( #next[ PUSH(N) ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <program> PGM </program>
+      <wordStack> WS => #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int N +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.dup]:
+      <k> ( #next[ DUP(N) ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> WS => WS [ ( N +Int -1 ) ] : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.swap]:
+      <k> ( #next[ SWAP(N) ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : WS => WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.add]:
+      <k> ( #next[ ADD ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => chop ( W0 +Int W1 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.sub]:
+      <k> ( #next[ SUB ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => chop ( W0 -Int W1 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.mul]:
+      <k> ( #next[ MUL ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => chop ( W0 *Int W1 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.and]:
+      <k> ( #next[ AND ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => W0 &Int W1 : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.or]:
+      <k> ( #next[ EVMOR ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => W0 |Int W1 : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.xor]:
+      <k> ( #next[ XOR ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => W0 xorInt W1 : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.iszero]:
+      <k> ( #next[ ISZERO ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : WS => bool2Word ( W0 ==Int 0 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.lt]:
+      <k> ( #next[ LT ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => bool2Word ( W0 <Int W1 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.gt]:
+      <k> ( #next[ GT ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => bool2Word ( W1 <Int W0 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+    rule [super.optimized.eq]:
+      <k> ( #next[ EQ ] => .K ) ... </k>
+      <useGas> false </useGas>
+      <wordStack> W0 : W1 : WS => bool2Word ( W0 ==Int W1 ) : WS </wordStack>
+      <pc> PCOUNT => PCOUNT +Int 1 </pc>
+      [priority(30)]
+
+endmodule
+```

src/kontrol/kdist/kontrol_lemmas.md

@@ -14,18 +14,6 @@ module KONTROL-AUX-LEMMAS
     imports MAP-SYMBOLIC
     imports SET-SYMBOLIC
 
-    syntax StepSort ::= Int
-                      | Bool
-                      | Bytes
-                      | Map
-                      | Set
- // -------------------------
-
-    syntax KItem ::= runLemma ( StepSort )
-                   | doneLemma( StepSort )
- // --------------------------------------
-    rule <k> runLemma(T) => doneLemma(T) ... </k>
-
     syntax Int ::= "ethMaxWidth" [macro]
     syntax Int ::= "ethUpperBound" [macro]
  // --------------------------------------

src/kontrol/kompile.py

@@ -63,6 +63,7 @@ def foundry_kompile(
         options.requires
         + ([KSRC_DIR / 'keccak.md'] if options.keccak_lemmas else [])
         + ([KSRC_DIR / 'kontrol_lemmas.md'] if options.auxiliary_lemmas else [])
+        + ([KSRC_DIR / 'evm_rule_optimizations.md'] if options.evm_rule_optimizations else [])
     )
     for r in tuple(requires):
         req = Path(r)
@@ -121,6 +122,7 @@ def foundry_kompile(
             imports=_imports,
             keccak_lemmas=options.keccak_lemmas,
             auxiliary_lemmas=options.auxiliary_lemmas,
+            evm_rule_optimizations=options.evm_rule_optimizations,
         )
 
         kevm = KEVM(
@@ -216,6 +218,7 @@ def _foundry_to_main_def(
     imports: dict[str, list[str]],
     keccak_lemmas: bool,
     auxiliary_lemmas: bool,
+    evm_rule_optimizations: bool,
 ) -> KDefinition:
     modules = [
         contract_to_verification_module(contract, empty_config, imports=imports[contract.name_with_path])
@@ -227,6 +230,7 @@ def _foundry_to_main_def(
             [KImport(mname) for mname in (_m.name for _m in modules)]
             + ([KImport('KECCAK-LEMMAS')] if keccak_lemmas else [])
             + ([KImport('KONTROL-AUX-LEMMAS')] if auxiliary_lemmas else [])
+            + ([KImport('EVM-RULE-OPTIMIZATIONS')] if evm_rule_optimizations else [])
         ),
     )
 

src/kontrol/options.py

@@ -839,6 +839,7 @@ class BuildOptions(LoggingOptions, KOptions, KGenOptions, KompileOptions, Foundr
     no_metadata: bool
     keccak_lemmas: bool
     auxiliary_lemmas: bool
+    evm_rule_optimizations: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -850,6 +851,7 @@ def default() -> dict[str, Any]:
             'no_metadata': False,
             'keccak_lemmas': True,
             'auxiliary_lemmas': False,
+            'evm_rule_optimizations': False,
         }
 
     @staticmethod