Hacktoberfest 2026:メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

Support `unsafe` for `to_module`

オープン
#4,754 コメント 0 件 リアクション 0 件 担当者 1 名 GitHub で見る

@Stevengre がすでに取り組んでいます。

2025年2月10日 から。

評価

この issue はまだ評価されていません。

説明

bug kast

Currently, the unsafe argument is only provided by _ml_constraint_to_bool which cannot be setup from the ouside. This can cause problem for printing kast with term like Exist, resulting in the following error info:

Traceback (most recent call last):
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/bin/kevm", line 6, in <module>
    sys.exit(main())
             ^^^^^^
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/__main__.py", line 102, in main
    execute(options)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/__main__.py", line 640, in exec_summarize
    analyze_proof('BALANCE_1', 1)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py", line 614, in analyze_proof
    summarizer.analyze_proof(str(proof_dir / f'{opcode}_SPEC'), node_id)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py", line 555, in analyze_proof
    self.summarize(proof)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py", line 549, in summarize
    for res_line in proof_show.show(proof, to_module=True):
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/proof/show.py", line 79, in show
    res_lines = self.kcfg_show.show(
                ^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/show.py", line 375, in show
    module = self.to_module(cfg, module_name, omit_cells=omit_cells)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/show.py", line 323, in to_module
    module = cfg.to_module(module_name)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 729, in to_module
    return KFlatModule(module_name, self.to_rules(priority=priority), imports=imports, att=att)
                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 717, in to_rules
    return [e.to_rule(_id, priority=priority) for e in self.edges()] + [
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 717, in <listcomp>
    return [e.to_rule(_id, priority=priority) for e in self.edges()] + [
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 243, in to_rule
    rule, _ = cterm_build_rule(
              ^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/cterm/cterm.py", line 411, in cterm_build_rule
    return build_rule(
           ^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 773, in build_rule
    init_constraints = [normalize_ml_pred(c) for c in init_constraints]
                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 773, in <listcomp>
    init_constraints = [normalize_ml_pred(c) for c in init_constraints]
                        ^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 207, in normalize_ml_pred
    return bool_to_ml_pred(simplify_bool(ml_pred_to_bool(pred)))
                                         ^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 170, in ml_pred_to_bool
    return _ml_constraint_to_bool(kast)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 125, in _ml_constraint_to_bool
    return notBool(_ml_constraint_to_bool(_kast.args[0]))
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 168, in _ml_constraint_to_bool
    raise ValueError(f'Could not convert ML predicate to sort Bool: {_kast}')
ValueError: Could not convert ML predicate to sort Bool: KApply(label=KLabel(name='#Exists', params=(KSort(name='CodeCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen0', sort=KSort(name='CodeCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='StorageCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen1', sort=KSort(name='StorageCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='OrigStorageCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen2', sort=KSort(name='OrigStorageCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='TransientStorageCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen3', sort=KSort(name='TransientStorageCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='NonceCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen4', sort=KSort(name='NonceCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='Int'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='BAL', sort=KSort(name='Int')), KApply(label=KLabel(name='#And', params=(KSort(name='GeneratedTopCell'),)), args=(KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='false', sort=KSort(name='Bool')), KApply(label=KLabel(name='AccountCellMap:in_keys', params=()), args=(KApply(label=KLabel(name='<acctID>', params=()), args=(KApply(label=KLabel(name='_modInt_', params=()), args=(KVariable(name='W0', sort=KSort(name='Int')), KToken(token='1461501637330902918203684832716283019655932542976', sort=KSort(name='Int')))),)), KVariable(name='AC1_1', sort=KSort(name='AccountCellMap')))))), KApply(label=KLabel(name='#And', params=(KSort(name='GeneratedTopCell'),)), args=(KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='false', sort=KSort(name='Bool')), KApply(label=KLabel(name='AccountCellMap:in_keys', params=()), args=(KApply(label=KLabel(name='<acctID>', params=()), args=(KVariable(name='W0', sort=KSort(name='Int')),)), KVariable(name='AC1_1', sort=KSort(name='AccountCellMap')))))), KApply(label=KLabel(name='#Equals', params=(KSort(name='AccountCellMap'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='DotAccountVar', sort=KSort(name='AccountCellMap')), KApply(label=KLabel(name='_AccountCellMap_', params=()), args=(KApply(label=KLabel(name='<account>', params=()), args=(KApply(label=KLabel(name='<acctID>', params=()), args=(KApply(label=KLabel(name='_modInt_', params=()), args=(KVariable(name='W0', sort=KSort(name='Int')), KToken(token='1461501637330902918203684832716283019655932542976', sort=KSort(name='Int')))),)), KApply(label=KLabel(name='<balance>', params=()), args=(KVariable(name='BAL', sort=KSort(name='Int')),)), KVariable(name='_Gen0', sort=KSort(name='CodeCell')), KVariable(name='_Gen1', sort=KSort(name='StorageCell')), KVariable(name='_Gen2', sort=KSort(name='OrigStorageCell')), KVariable(name='_Gen3', sort=KSort(name='TransientStorageCell')), KVariable(name='_Gen4', sort=KSort(name='NonceCell')))), KVariable(name='AC1_1', sort=KSort(name='AccountCellMap')))))))))))))))))))))

We should add unsafe argument according to this error trace.

主要言語
Python
スター
598
フォーク
164
PR マージ指標
30日以内にマージされた PR はありません

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

runtimeverification/k のほかの issue

runtimeverification/k の issue をすべて見る

似ている issue

Python の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。