print nodes and add summarize function to generate optimized rules fo…

…r instructions
runtimeverification · Jan 8, 2025 · 38825bc · 38825bc
1 parent 8d99d78
commit 38825bc
Showing 1 changed file with 17 additions and 3 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py
@@ -51,11 +51,18 @@ def build_spec(
         cterm = CTerm(self.kevm.definition.empty_config(KSort('GeneratedTopCell')))
 
         # construct the initial substitution
-        opcode = KVariable('OP_CODE', KSort('OpCode'))
+        # opcode = KVariable('OP_CODE', KSort('OpCode'))
+        opcode = KVariable('OP_CODE', KSort('BinStackOp'))
         next_opcode = KApply('#next[_]_EVM_InternalOp_MaybeOpCode', opcode)
         _init_subst: dict[str, KInner] = {'K_CELL': KSequence([next_opcode, KVariable('K_CELL')])}
         _init_subst['PROGRAM_CELL'] = self.kevm.bytes_empty()
         init_subst = CSubst(Subst(_init_subst), ())
+        # TODO: following provides some special cases that cannot be handled automatically
+        # Error Message:
+        # Runtime error | code: -32002 | data: {'context': 'CallStack (from HasCallStack):\n  error, called at src/Kore/Rewrite/Function/Evaluator.hs:377:6 in kore-0.1.104-CWw3vBaRpxI3Spyxy9LUQ8:Kore.Rewrite.Function.Evaluator', 'error': 'Error: missing hook\nSymbol\n    LblisValidPoint\'LParUndsRParUnds\'KRYPTO\'Unds\'Bool\'Unds\'G1Point{}\ndeclared with attribute\n    hook{}("KRYPTO.bn128valid")\nWe don\'t recognize that hook and it was not given any rules.\nPlease open a feature request at\n    https://github.com/runtimeverification/haskell-backend/issues\nand include the text of this message.\nWorkaround: Give rules for LblisValidPoint\'LParUndsRParUnds\'KRYPTO\'Unds\'Bool\'Unds\'G1Point{}'}
+        # Analysis: need hook in Haskell backend for KRYPTO.bn128valid
+        # Temp Solution: skip the PrecompiledOp for now
+
 
         # construct the final substitution
         _final_subst: dict[str, KInner] = {vname: KVariable('FINAL_' + vname) for vname in cterm.free_vars}
@@ -149,6 +156,7 @@ def create_kcfg_explore() -> KCFGExplore:
 
             res_lines = proof_show.show(
                 proof,
+                nodes= [node.id for node in proof.kcfg.nodes],
             )
 
             return passed, res_lines
@@ -157,5 +165,11 @@ def create_kcfg_explore() -> KCFGExplore:
         for line in res_lines:
             print(line)
 
-    def summarize(self) -> None:
-        pass
+    def summarize(self, proof: APRProof) -> None:
+        proof.minimize_kcfg(KEVMSemantics(), False)
+        node_printer = kevm_node_printer(self.kevm, proof)
+        proof_show = APRProofShow(self.kevm, node_printer=node_printer)
+        for res_line in proof_show.show(proof, to_module=True):
+            print(res_line)
+
+