back up to keep my thinking of debuging

Author: Stevengre

kevm-pyk/src/kevm_pyk/__main__.py

@@ -32,7 +32,7 @@
 from pyk.proof.tui import APRProofViewer
 from pyk.utils import FrozenDict, hash_str, single
 
-from kevm_pyk.summarizer import get_todo_list, summarize
+from kevm_pyk.summarizer import KEVMSummarizer, get_todo_list, summarize
 
 from . import VERSION, config
 from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
@@ -637,10 +637,18 @@ def exec_kast(options: KastOptions) -> None:
 
 
 def exec_summarize(options: ProveOptions) -> None:
+    proof_dir = Path(__file__).parent / 'proofs'
+    save_directory = Path(__file__).parent / 'summaries'
+    p = APRProof.read_proof_data(Path(__file__).parent / 'proofs', 'STOP-SUMMARY-16-TO-10')
+    # print('proof initial state -------------------------------')
+    # print(p.kcfg.node(p.init).cterm)
+    summarizer = KEVMSummarizer(proof_dir, save_directory)
+    summarizer.explore(p)
+    
     # batch_summarize()
-    next_opcode = get_todo_list()
-    _LOGGER.info(f'summarizing {next_opcode}')
-    summarize(next_opcode[0])
+    # next_opcode = get_todo_list()
+    # _LOGGER.info(f'summarizing {next_opcode}')
+    # summarize(next_opcode[0])
     # analyze_proof('CREATE_3', 3)
 
 

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -471,7 +471,7 @@ def build_spec(self, opcode: KApply, stack_needed: int, id_str: str = '') -> APR
         _LOGGER.debug(proof.kcfg.nodes[0].cterm.to_dict())
         return proof
 
-    def explore(self, proof: APRProof) -> None:
+    def explore(self, proof: APRProof) -> bool:
         """
         Execute the specification to explore the KCFG for all possible instructions.
         """
@@ -568,6 +568,7 @@ def create_kcfg_explore() -> KCFGExplore:
             for line in res_lines:
                 f.write(line)
                 f.write('\n')
+        return passed
 
     def summarize(self, proof: APRProof, merge: bool = False) -> None:
         # TODO: need customized minimization rules, maybe
@@ -625,12 +626,13 @@ def batch_summarize(num_processes: int = 4) -> None:
     _LOGGER.info('Batch summarization completed')
 
 
-def summarize(opcode_symbol: str) -> None:
+def summarize(opcode_symbol: str) -> tuple[KEVMSummarizer, list[APRProof]]:
     proof_dir = Path(__file__).parent / 'proofs'
     save_directory = Path(__file__).parent / 'summaries'
     summarizer = KEVMSummarizer(proof_dir, save_directory)
     needs = stack_needed(opcode_symbol)
     opcode = OPCODES[opcode_symbol]
+    proofs = []
     for need in needs:
         if len(needs) > 1:
             opcode = KApply(opcode.label.name, KToken(str(need), KSort('Int')))
@@ -642,6 +644,8 @@ def summarize(opcode_symbol: str) -> None:
             )
             summarizer.explore(proof)
             summarizer.summarize(proof)
+            proof.write_proof_data()
+            proofs.append(proof)
 
             proof = summarizer.build_spec(opcode, need, id_str='_TRUE')
             _subst = {'K_CELL': KSequence([KApply('#endBasicBlock_EVM_InternalOp'), KVariable('K_CELL')])}
@@ -653,15 +657,22 @@ def summarize(opcode_symbol: str) -> None:
             proof.kcfg.let_node(2, cterm=subst(proof.kcfg.get_node(2).cterm), attrs=proof.kcfg.get_node(2).attrs)
             summarizer.explore(proof)
             summarizer.summarize(proof)
+            proof.write_proof_data()
+            proofs.append(proof)
         elif opcode_symbol == 'LOG':
             need += 2
             proof = summarizer.build_spec(opcode, need)
             summarizer.explore(proof)
             summarizer.summarize(proof)
+            proof.write_proof_data()
+            proofs.append(proof)
         else:
             proof = summarizer.build_spec(opcode, need)
             summarizer.explore(proof)
             summarizer.summarize(proof)
+            proof.write_proof_data()
+            proofs.append(proof)
+    return summarizer, proofs
     # summarizer.analyze_proof(proof_dir / 'STOP_SPEC')
     # validation: generate them as claims and call kevm prove.
 
@@ -671,3 +682,10 @@ def analyze_proof(opcode: str, node_id: int) -> None:
     save_directory = Path(__file__).parent / 'summaries'
     summarizer = KEVMSummarizer(proof_dir, save_directory)
     summarizer.analyze_proof(proof_dir / f'{opcode}_SPEC', node_id)
+
+def debug_proof(proof_id: str) -> None:
+    proof_dir = Path(__file__).parent / 'proofs'
+    save_directory = Path(__file__).parent / 'summaries'
+    summarizer = KEVMSummarizer(proof_dir, save_directory)
+    proof = APRProof.read_proof_data(proof_dir, proof_id)
+    

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

@@ -0,0 +1,76 @@
+from ast import Import
+from kevm_pyk.summarizer import OPCODES, get_summary_status, OPCODES_SUMMARY_STATUS, summarize
+import pytest
+from pyk.kcfg import KCFG
+from pyk.kast.inner import KVariable, Subst
+from pyk.kast.outer import KFlatModule, KRequire, KImport
+from pyk.kast.att import Atts
+from pyk.cterm import CSubst
+from pyk.proof.reachability import APRProof
+
+@pytest.mark.parametrize('opcode', OPCODES.keys())
+def test_summarize(opcode: str) -> None:
+    if get_summary_status(opcode) != 'PASSED':
+        pytest.skip(f'{opcode} status: {OPCODES_SUMMARY_STATUS[opcode]}')
+    if opcode == 'STOP':
+        summarizer, proofs = summarize(opcode)
+        for proof in proofs:
+            claims = []
+            
+            # no pending, failing, bounded nodes in the proof
+            for leaf in proof.kcfg.leaves:
+                assert not proof.is_pending(leaf.id)
+                assert not proof.kcfg.is_stuck(leaf.id)
+                assert not proof.kcfg.is_vacuous(leaf.id)
+                assert not proof.is_bounded(leaf.id)
+            
+            # only one successor from the initial node in the proof
+            successors = proof.kcfg.successors(proof.init)
+            assert len(successors) == 1
+            successor = successors[0]
+            
+            # only one edge to the terminal node
+            if isinstance(successor, KCFG.Split):
+                targets = successor.targets
+                assert len(proof.kcfg.edges()) == len(targets)
+                for target in targets:
+                    successors = proof.kcfg.successors(target.id)
+                    assert len(successors) == 1
+                    edge = successors[0]
+                    assert isinstance(edge, KCFG.Edge)
+                    assert proof.is_terminal(edge.target.id)
+                    claims.append(edge.to_rule(f'{opcode}-SUMMARY', claim = True))
+            else:
+                assert len(proof.kcfg.edges()) == 1
+                assert isinstance(successor, KCFG.Edge)
+                assert proof.is_terminal(successor.target.id)
+                claims.append(successor.to_rule(f'{opcode}-SUMMARY', claim = True))
+                
+            # prove the correctness of the summary
+            # KRequire('edsl.md'),
+            # module = KFlatModule(f'{opcode}-SUMMARY', claims)
+            # with open(summarizer.save_directory / proof.id / f'{opcode.lower()}-summary.k', 'w') as f:
+            #     res_lines = 'requires "edsl.md"\n'
+            #     res_lines += summarizer.kevm.pretty_print(module)
+            #     splited_lines = res_lines.split('\n')
+            #     splited_lines.insert(2, '    imports public EDSL')
+            #     res_lines = '\n'.join(splited_lines)
+            #     f.write(res_lines)
+                
+            # int = 0
+            # print(len(claims))
+            # proof_result = summarizer.explore(APRProof.from_claim(summarizer.kevm.definition, claims[2], {}, summarizer.proof_dir))
+            # print(proof_result)
+            for claim in claims:
+                assert summarizer.explore(APRProof.from_claim(summarizer.kevm.definition, claim, {}, summarizer.proof_dir))
+            #     # TODO: fix the sort issue caused by `APRProof.from_claim`
+            #     # print(f'validating {claim.att[Atts.LABEL]}')
+            #     # _subst = {'_USEGAS_CELL': KVariable('_USEGAS_CELL', sort = 'Bool')}
+            #     # subst = CSubst(Subst(_subst), ())
+            #     summary_proof = APRProof.from_claim(summarizer.kevm.definition, claim, {}, summarizer.proof_dir)
+            #     # summary_proof.kcfg.let_node(1, cterm = subst(summary_proof.kcfg.get_node(1).cterm), attrs = summary_proof.kcfg.get_node(1).attrs)
+            #     proof_result = summarizer.explore(summary_proof)
+            #     # print(f'{claim.att[Atts.LABEL]} proof result: {proof_result}')
+            #     assert proof_result
+    else:
+        pytest.skip(f'{opcode} ignored')

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

@@ -0,0 +1,2 @@
+new_init_constraints: [KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='true', sort=KSort(name='Bool')), KVariable(name='_USEGAS_CELL', sort=KSort(name='Bool')))), KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='true', sort=KSort(name='Bool')), KApply(label=KLabel(name='_<=Gas__GAS-SYNTAX_Bool_Gas_Gas', params=()), args=(KApply(label=KLabel(name='_<_>_SCHEDULE_Int_ScheduleConst_Schedule', params=()), args=(KApply(label=KLabel(name='Gzero_SCHEDULE_ScheduleConst', params=()), args=()), KVariable(name='SCHEDULE_CELL', sort=KSort(name='Schedule')))), KVariable(name='GAS_CELL', sort=KSort(name='Gas'))))))]
+Proof timing STOP-SUMMARY-16-TO-10: 59.61101531982422s