Update dependency: deps/k_release

deps/k_release

@@ -1 +1 @@
-7.1.253
+7.1.259

flake.nix

@@ -2,7 +2,7 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.253";
+    k-framework.url = "github:runtimeverification/k/v7.1.259";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";

kevm-pyk/pyproject.toml

@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.253"
+kframework = "7.1.259"
 tomlkit = "^0.11.6"
 frozendict = "^2.4.6"
 

kevm-pyk/src/kevm_pyk/__main__.py

@@ -538,15 +538,14 @@ def exec_show_kcfg(options: ShowKCFGOptions) -> None:
         nodes = list(nodes) + [node.id for node in proof.failing]
 
     node_printer = kevm_node_printer(kevm, proof)
-    proof_show = APRProofShow(kevm, node_printer=node_printer)
+    proof_show = APRProofShow(kevm.definition, node_printer=node_printer)
 
     res_lines = proof_show.show(
         proof,
         nodes=nodes,
         node_deltas=options.node_deltas,
         to_module=options.to_module,
         minimize=options.minimize,
-        sort_collections=options.sort_collections,
     )
 
     if options.failure_info:

kevm-pyk/src/kevm_pyk/kevm.py

@@ -5,6 +5,7 @@
 from typing import TYPE_CHECKING, NamedTuple
 
 from pyk.cterm import CTerm, CTermSymbolic
+from pyk.cterm.show import CTermShow
 from pyk.kast import KInner
 from pyk.kast.inner import (
     KApply,
@@ -25,7 +26,7 @@
 from pyk.kast.prelude.ml import mlEqualsFalse, mlEqualsTrue
 from pyk.kast.prelude.string import stringToken
 from pyk.kast.prelude.utils import token
-from pyk.kast.pretty import paren
+from pyk.kast.pretty import PrettyPrinter, paren
 from pyk.kcfg.kcfg import KCFGExtendResult, Step
 from pyk.kcfg.semantics import DefaultSemantics
 from pyk.kcfg.show import NodePrinter
@@ -697,8 +698,8 @@ def end_basic_block() -> KInner:
 class KEVMNodePrinter(NodePrinter):
     kevm: KEVM
 
-    def __init__(self, kevm: KEVM):
-        NodePrinter.__init__(self, kevm)
+    def __init__(self, kevm: KEVM, cterm_show: CTermShow, full_printer: bool = True):
+        NodePrinter.__init__(self, cterm_show, full_printer=full_printer)
         self.kevm = kevm
 
     def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
@@ -708,14 +709,15 @@ def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
 
 
 class KEVMAPRNodePrinter(KEVMNodePrinter, APRProofNodePrinter):
-    def __init__(self, kevm: KEVM, proof: APRProof):
-        KEVMNodePrinter.__init__(self, kevm)
-        APRProofNodePrinter.__init__(self, proof, kevm)
+    def __init__(self, kevm: KEVM, cterm_show: CTermShow, proof: APRProof, full_printer: bool = True):
+        KEVMNodePrinter.__init__(self, kevm, cterm_show, full_printer=full_printer)
+        APRProofNodePrinter.__init__(self, proof, cterm_show, full_printer=full_printer)
 
 
-def kevm_node_printer(kevm: KEVM, proof: APRProof) -> NodePrinter:
+def kevm_node_printer(kevm: KEVM, proof: APRProof, full_printer: bool = True) -> NodePrinter:
+    cterm_show = CTermShow(PrettyPrinter(kevm.definition, patch_symbol_table=KEVM._kevm_patch_symbol_table).print)
     if type(proof) is APRProof:
-        return KEVMAPRNodePrinter(kevm, proof)
+        return KEVMAPRNodePrinter(kevm, cterm_show, proof, full_printer=full_printer)
     raise ValueError(f'Cannot build NodePrinter for proof type: {type(proof)}')
 
 

kevm-pyk/src/kevm_pyk/kompile.py

@@ -224,7 +224,7 @@ def _kompile_haskell() -> None:
 
 
 def lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]:
-    ccopts = ['-std=c++17']
+    ccopts = ['-std=c++20']
 
     if debug_build:
         ccopts += ['-g']

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -613,7 +613,7 @@ def show_proof(
         omit_cells: Iterable[str] = (),
     ) -> list[str]:
         node_printer = kevm_node_printer(self.kevm, proof)
-        proof_show = APRProofShow(self.kevm, node_printer=node_printer)
+        proof_show = APRProofShow(self.kevm.definition, node_printer=node_printer)
         return proof_show.show(
             proof,
             nodes=nodes,
@@ -841,7 +841,7 @@ def create_kcfg_explore() -> KCFGExplore:
 
     def _to_rules(self, proof: APRProof) -> list[KRule]:
         krules = []
-        module = APRProofShow(self.kevm, kevm_node_printer(self.kevm, proof)).kcfg_show.to_module(proof.kcfg)
+        module = APRProofShow(self.kevm.definition, kevm_node_printer(self.kevm, proof)).kcfg_show.to_module(proof.kcfg)
         for krule in module.sentences:
             assert isinstance(krule, KRule), f'Unexpected sentence type: {type(krule)}\n{self.kevm.pretty_print(krule)}'
             body, requires, ensures, atts = krule.body, krule.requires, krule.ensures, krule.att

kevm-pyk/src/tests/integration/test_prove.py

@@ -425,7 +425,7 @@ def _validate_proofs(kevm: KEVM, kore_rpc_command: tuple[str, ...], proofs: list
             initialize_apr_proof(kcfg_explore.cterm_symbolic, proof)
             prover.advance_proof(proof, max_iterations=20)
             node_printer = kevm_node_printer(kevm, proof)
-            proof_show = APRProofShow(kevm, node_printer=node_printer)
+            proof_show = APRProofShow(kevm.definition, node_printer=node_printer)
             proof_display = '\n'.join('    ' + line for line in proof_show.show(proof))
             _LOGGER.info(f'Proof {proof.id}:\n{proof_display}')
             assert proof.passed