summarize instructions one by one

runtimeverification · Jan 9, 2025 · 82ace9a · 82ace9a
1 parent e914f89
commit 82ace9a
Showing 1 changed file with 8 additions and 3 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py
@@ -5,7 +5,7 @@
 from typing import TYPE_CHECKING
 
 from pyk.cterm import CSubst, CTerm, CTermSymbolic, cterm_build_claim
-from pyk.kast.inner import KApply, KInner, KSequence, KVariable, Subst
+from pyk.kast.inner import KApply, KInner, KSequence, KToken, KVariable, Subst
 from pyk.kast.outer import KSort
 from pyk.kcfg import KCFGExplore
 from pyk.kdist import kdist
@@ -52,7 +52,8 @@ def build_spec(
 
         # construct the initial substitution
         # opcode = KVariable('OP_CODE', KSort('OpCode'))
-        opcode = KVariable('OP_CODE', KSort('BinStackOp'))
+        # opcode = KVariable('OP_CODE', KSort('BinStackOp'))
+        opcode = KApply('STOP_EVM_NullStackOp')
         next_opcode = KApply('#next[_]_EVM_InternalOp_MaybeOpCode', opcode)
         _init_subst: dict[str, KInner] = {'K_CELL': KSequence([next_opcode, KVariable('K_CELL')])}
         init_subst = CSubst(Subst(_init_subst), ())
@@ -158,7 +159,11 @@ def create_kcfg_explore() -> KCFGExplore:
 
             return passed, res_lines
 
-        _, res_lines = _init_and_run_proof(proof)
+        passed, res_lines = _init_and_run_proof(proof)
+        if passed:
+            print(f'Proof {proof.id} Passed')
+        else:
+            print(f'Proof {proof.id} Failed')
         for line in res_lines:
             print(line)