Option to emit summaries as rules instead of claims (#793)

* kontrol/prove: use factored out Minimizer

* kontrol/{cli,options,foundry}: add option to generate KEVM rules from output

* kontrol/{options,cli,foundry}: add option --minimize-kcfg to kontrol show

* kontrol/foundry: respect option --minimize for reducing configuration size on --to-kevm-[rules|claims]

* kontrol/foundry: rename optional parameter definition => defunc_with

src/kontrol/cli.py

@@ -605,6 +605,13 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Generate a K module which can be run directly as KEVM claims for the given KCFG (best-effort).',
     )
+    show_args.add_argument(
+        '--to-kevm-rules',
+        dest='to_kevm_rules',
+        default=None,
+        action='store_true',
+        help='Generate a K module which can be used to optimize KEVM execution (best-effort).',
+    )
     show_args.add_argument(
         '--kevm-claim-dir',
         dest='kevm_claim_dir',
@@ -625,6 +632,13 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='When printing nodes, always show full bytecode in  code and program cells, and do not hide jumpDests cell.',
     )
+    show_args.add_argument(
+        '--minimize-kcfg',
+        dest='minimize_kcfg',
+        default=None,
+        action='store_true',
+        help='Run KCFG minimization routine before displaying it.',
+    )
 
     command_parser.add_parser(
         'to-dot',

src/kontrol/foundry.py

@@ -24,6 +24,7 @@
 from pyk.kast.manip import cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down
 from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire
 from pyk.kcfg import KCFG
+from pyk.kcfg.minimize import KCFGMinimizer
 from pyk.prelude.bytes import bytesToken
 from pyk.prelude.collections import map_empty
 from pyk.prelude.k import DOTS
@@ -785,6 +786,9 @@ def foundry_show(
     )
     proof_show = APRProofShow(foundry.kevm, node_printer=node_printer)
 
+    if options.minimize_kcfg:
+        KCFGMinimizer(proof.kcfg).minimize()
+
     res_lines = proof_show.show(
         proof,
         nodes=nodes,
@@ -811,7 +815,7 @@ def foundry_show(
             res_lines += print_failure_info(proof, kcfg_explore, options.counterexample_info)
             res_lines += Foundry.help_info()
 
-    if options.to_kevm_claims:
+    if options.to_kevm_claims or options.to_kevm_rules:
         _foundry_labels = [
             prod.klabel
             for prod in foundry.kevm.definition.all_modules_dict['FOUNDRY-CHEAT-CODES'].productions
@@ -822,7 +826,10 @@ def _remove_foundry_config(_cterm: CTerm) -> CTerm:
             kevm_config_pattern = KApply(
                 '<generatedTop>',
                 [
-                    KApply('<foundry>', [KVariable('KEVM_CELL'), KVariable('CHEATCODES_CELL')]),
+                    KApply(
+                        '<foundry>',
+                        [KVariable('KEVM_CELL'), KVariable('CHEATCODES_CELL'), KVariable('KEVMTRACING_CELL')],
+                    ),
                     KVariable('GENERATEDCOUNTER_CELL'),
                 ],
             )
@@ -849,26 +856,34 @@ def _collect_klabel(_k: KInner) -> None:
         # Due to bug in KCFG.replace_node: https://github.com/runtimeverification/pyk/issues/686
         proof.kcfg = KCFG.from_dict(proof.kcfg.to_dict())
 
-        claims = [edge.to_rule('BASIC-BLOCK', claim=True) for edge in proof.kcfg.edges()]
-        claims = [claim for claim in claims if not _contains_foundry_klabel(claim.body)]
-        claims = [
-            claim for claim in claims if not KEVMSemantics().is_terminal(CTerm.from_kast(extract_lhs(claim.body)))
+        sentences = [
+            edge.to_rule(
+                'BASIC-BLOCK',
+                claim=(not options.to_kevm_rules),
+                defunc_with=foundry.kevm.definition,
+                minimize=options.minimize,
+            )
+            for edge in proof.kcfg.edges()
+        ]
+        sentences = [sent for sent in sentences if not _contains_foundry_klabel(sent.body)]
+        sentences = [
+            sent for sent in sentences if not KEVMSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
         ]
-        if len(claims) == 0:
-            _LOGGER.warning(f'No claims retained for proof {proof.id}')
+        if len(sentences) == 0:
+            _LOGGER.warning(f'No claims or rules retained for proof {proof.id}')
 
         else:
             module_name = Contract.escaped(proof.id.upper() + '-SPEC', '')
-            module = KFlatModule(module_name, sentences=claims, imports=[KImport('VERIFICATION')])
+            module = KFlatModule(module_name, sentences=sentences, imports=[KImport('VERIFICATION')])
             defn = KDefinition(module_name, [module], requires=[KRequire('verification.k')])
 
             defn_lines = foundry.kevm.pretty_print(defn, in_module='EVM').split('\n')
 
             res_lines += defn_lines
 
             if options.kevm_claim_dir is not None:
-                kevm_claims_file = options.kevm_claim_dir / (module_name.lower() + '.k')
-                kevm_claims_file.write_text('\n'.join(line.rstrip() for line in defn_lines))
+                kevm_sentences_file = options.kevm_claim_dir / (module_name.lower() + '.k')
+                kevm_sentences_file.write_text('\n'.join(line.rstrip() for line in defn_lines))
 
     return '\n'.join([line.rstrip() for line in res_lines])
 

src/kontrol/options.py

@@ -571,19 +571,23 @@ class ShowOptions(
 ):
     omit_unstable_output: bool
     to_kevm_claims: bool
+    to_kevm_rules: bool
     kevm_claim_dir: Path | None
     use_hex_encoding: bool
     expand_config: bool
+    minimize_kcfg: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
         return {
             'omit_unstable_output': False,
             'to_kevm_claims': False,
+            'to_kevm_rules': False,
             'kevm_claim_dir': None,
             'use_hex_encoding': False,
             'counterexample_info': True,
             'expand_config': False,
+            'minimize_kcfg': False,
         }
 
     @staticmethod