Update dependency: deps/k_release (#2572)

* deps/k_release: Set Version 7.1.103

* Set Version: 1.0.678

* kevm-pyk/: sync poetry files pyk version 7.1.103

* flake.{nix,lock}: update Nix derivations

* renaming parameters

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>

Author: 4 people

deps/k_release

@@ -1 +1 @@
-7.1.102
+7.1.103

flake.lock

@@ -2,11 +2,11 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.102";
+    k-framework.url = "github:runtimeverification/k/v7.1.103";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
-    pyk.url = "github:runtimeverification/k/v7.1.102?dir=pyk";
+    pyk.url = "github:runtimeverification/k/v7.1.103?dir=pyk";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
     blockchain-k-plugin = {

flake.nix

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.677"
+version = "1.0.678"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.102"
+kframework = "7.1.103"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

kevm-pyk/poetry.lock

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.677'
+VERSION: Final = '1.0.678'

kevm-pyk/pyproject.toml

@@ -301,7 +301,8 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
             kore_rpc_command=kore_rpc_command,
             smt_timeout=options.smt_timeout,
             smt_retry_limit=options.smt_retry_limit,
-            trace_rewrites=options.trace_rewrites,
+            log_succ_rewrites=options.log_succ_rewrites,
+            log_fail_rewrites=options.log_fail_rewrites,
             fallback_on=options.fallback_on,
             interim_simplification=options.interim_simplification,
             no_post_exec_simplify=(not options.post_exec_simplify),
@@ -319,7 +320,12 @@ def create_kcfg_explore() -> KCFGExplore:
                     bug_report_id=bug_report_id,
                     dispatch=dispatch,
                 )
-                cterm_symbolic = CTermSymbolic(client, kevm.definition, trace_rewrites=options.trace_rewrites)
+                cterm_symbolic = CTermSymbolic(
+                    client,
+                    kevm.definition,
+                    log_succ_rewrites=options.log_succ_rewrites,
+                    log_fail_rewrites=options.log_fail_rewrites,
+                )
                 return KCFGExplore(
                     cterm_symbolic,
                     kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas),
@@ -482,7 +488,8 @@ def exec_section_edge(options: SectionEdgeOptions) -> None:
         kore_rpc_command=kore_rpc_command,
         smt_timeout=options.smt_timeout,
         smt_retry_limit=options.smt_retry_limit,
-        trace_rewrites=options.trace_rewrites,
+        log_succ_rewrites=options.log_succ_rewrites,
+        log_fail_rewrites=options.log_fail_rewrites,
         llvm_definition_dir=llvm_definition_dir,
     ) as kcfg_explore:
         node_ids = kcfg_explore.section_edge(

kevm-pyk/src/kevm_pyk/__init__.py

@@ -300,7 +300,8 @@ def get_argument_type() -> dict[str, Callable]:
 
 
 class RPCOptions(Options):
-    trace_rewrites: bool
+    log_succ_rewrites: bool
+    log_fail_rewrites: bool
     kore_rpc_command: str | None
     use_booster: bool
     fallback_on: list[FallbackReason]
@@ -313,7 +314,8 @@ class RPCOptions(Options):
     @staticmethod
     def default() -> dict[str, Any]:
         return {
-            'trace_rewrites': False,
+            'log_succ_rewrites': True,
+            'log_fail_rewrites': False,
             'kore_rpc_command': None,
             'use_booster': True,
             'fallback_on': [],
@@ -959,8 +961,15 @@ def display_args(self) -> ArgumentParser:
     def rpc_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
         args.add_argument(
-            '--trace-rewrites',
-            dest='trace_rewrites',
+            '--no-log-rewrites',
+            dest='log_succ_rewrites',
+            default=None,
+            action='store_false',
+            help='Do not log traces of any simplification and rewrite rule application.',
+        )
+        args.add_argument(
+            '--log-fail-rewrites',
+            dest='log_fail_rewrites',
             default=None,
             action='store_true',
             help='Log traces of all simplification and rewrite rule applications.',

kevm-pyk/src/kevm_pyk/__main__.py

@@ -348,7 +348,8 @@ def legacy_explore(
     haskell_log_entries: Iterable[str] = (),
     haskell_threads: int | None = None,
     log_axioms_file: Path | None = None,
-    trace_rewrites: bool = False,
+    log_succ_rewrites: bool = True,
+    log_fail_rewrites: bool = True,
     start_server: bool = True,
     maude_port: int | None = None,
     fallback_on: Iterable[FallbackReason] | None = None,
@@ -377,7 +378,9 @@ def legacy_explore(
             no_post_exec_simplify=no_post_exec_simplify,
         ) as server:
             with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=bug_report_id) as client:
-                cterm_symbolic = CTermSymbolic(client, kprint.definition, trace_rewrites=trace_rewrites)
+                cterm_symbolic = CTermSymbolic(
+                    client, kprint.definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+                )
                 yield KCFGExplore(cterm_symbolic, kcfg_semantics=kcfg_semantics, id=id)
     else:
         if port is None:
@@ -396,5 +399,7 @@ def legacy_explore(
         with KoreClient(
             'localhost', port, bug_report=bug_report, bug_report_id=bug_report_id, dispatch=dispatch
         ) as client:
-            cterm_symbolic = CTermSymbolic(client, kprint.definition, trace_rewrites=trace_rewrites)
+            cterm_symbolic = CTermSymbolic(
+                client, kprint.definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+            )
             yield KCFGExplore(cterm_symbolic, kcfg_semantics=kcfg_semantics, id=id)

kevm-pyk/src/kevm_pyk/cli.py

@@ -1 +1 @@
-1.0.677
+1.0.678