Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

`fast_check_subsumption` causes `Could not convert ML predicate to sort Bool` error

Aperta
  • Qualcosa non va?
#2,290 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
25/100
Tipo di issue
Bug
Chiarezza
Da chiarire
Stato di attività
Ferma
Ambito
devtools

Direzione di ricerca

Riproducete il malfunzionamento con i due comandi kevm kompile-spec e kevm prove usando tests/specs/erc20/verification.k e tests/specs/erc20/hkg/transferFrom-failure-2-spec.k. Leggete kevm_pyk/utils.py e gli entry point referenziati pyk/proof/reachability.py, pyk/kcfg/explore.py e pyk/kast/manip.py; il lavoro è completato quando il percorso fast_check_subsumption non produce più il malfunzionamento di conversione del predicato ML segnalato.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

bug

Related: https://github.com/runtimeverification/evm-semantics/pull/2287

fast_check_subsumption = True was introduced in https://github.com/runtimeverification/evm-semantics/pull/2243, causing failures in erc20 claims in CI tests. As @tothtamas28 found out, it's causing the following issue when running

poetry -C kevm-pyk run -- kevm kompile-spec tests/specs/erc20/verification.k --main-module VERIFICATION --output definition
poetry -C kevm-pyk run -- kevm prove tests/specs/erc20/hkg/transferFrom-failure-2-spec.k --definition definition --spec-module TRANSFERFROM-FAILURE-2-SPEC  --verbose --use-booster

Output (the interesting part):

INFO 2024-02-08 14:47:50,556 pyk.ktool.kprint - Invoking kore_to_kast
ERROR 2024-02-08 14:47:50,607 kevm_pyk.utils - Proof crashed: f0d4602717667cc05239620de33a8499dfb5c725aa4bcfa12a98ff90d1a94187
Could not convert ML predicate to sort Bool: KApply(label=KLabel(name='#Ceil', params=(KSort(name='Map'), KSort(name='GeneratedTopCell'))), args=(KApply(label=KLabel(name='_Map_', params=()), args=(KVariable(name='ORIGSTORAGE_CELL_311d596d', sort=KSort(name='Map')), KVariable(name='ORIGSTORAGE_CELL_a1996eba', sort=KSort(name='Map')))),))
Traceback (most recent call last):
  File "/home/ttoth/git/evm-semantics/kevm-pyk/src/kevm_pyk/utils.py", line 132, in run_prover
    prover.advance_proof(
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 863, in advance_proof
    self.save_failure_info()
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 868, in save_failure_info
    self.proof.failure_info = self.failure_info()
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 871, in failure_info
    return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
  File "/home/ttoth/git/pyk/src/pyk/proof/reachability.py", line 940, in from_proof
    _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
  File "/home/ttoth/git/pyk/src/pyk/kcfg/explore.py", line 265, in implication_failure_reason
    negative_cell_constraints = list(filter(_is_negative_cell_subst, antecedent.constraints))
  File "/home/ttoth/git/pyk/src/pyk/kcfg/explore.py", line 216, in _is_negative_cell_subst
    constraint_bool = ml_pred_to_bool(constraint)
  File "/home/ttoth/git/pyk/src/pyk/kast/manip.py", line 161, in ml_pred_to_bool
    return _ml_constraint_to_bool(kast)
  File "/home/ttoth/git/pyk/src/pyk/kast/manip.py", line 159, 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='#Ceil', params=(KSort(name='Map'), KSort(name='GeneratedTopCell'))), args=(KApply(label=KLabel(name='_Map_', params=()), args=(KVariable(name='ORIGSTORAGE_CELL_311d596d', sort=KSort(name='Map')), KVariable(name='ORIGSTORAGE_CELL_a1996eba', sort=KSort(name='Map')))),))

fast_check_subsumption has been temporarily set to False in https://github.com/runtimeverification/evm-semantics/pull/2287 to unblock pyk upgrade, but we should further investigate the failures associated with this option.

Lingua principale
KCL
Stelle
595
Fork
159
Merge medio
4g 3h
PR unite (30g)
1

Preparare l'ambiente

Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di runtimeverification/evm-semantics

Tutte le issue di runtimeverification/evm-semantics

Issue simili

Altre issue su DevTools

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.