From 4aeb0c3ffef960bcd12222ae77766962071a48c2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 22 Jan 2025 15:19:41 +0000 Subject: [PATCH] finish the test process on `STOP` --- .../src/tests/integration/test_summarize.py | 23 ------------------- xx | 2 -- 2 files changed, 25 deletions(-) delete mode 100644 xx diff --git a/kevm-pyk/src/tests/integration/test_summarize.py b/kevm-pyk/src/tests/integration/test_summarize.py index a69b4954c2..d92353c8ab 100644 --- a/kevm-pyk/src/tests/integration/test_summarize.py +++ b/kevm-pyk/src/tests/integration/test_summarize.py @@ -47,30 +47,7 @@ def test_summarize(opcode: str) -> None: 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') diff --git a/xx b/xx deleted file mode 100644 index 82658349bb..0000000000 --- a/xx +++ /dev/null @@ -1,2 +0,0 @@ -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