Update dependency: deps/pyk_release

[rv-jenkins]

No description provided.

[palinatolmach]

@tothtamas28 @ehildenb this PR is failing on erc20 tests starting from pyk version 0.1.616 (https://github.com/runtimeverification/pyk/releases/tag/v0.1.616), which enables processing of claims with no labels. Is it possible that the claims that are now failing are ill-formed, and just haven't been tested before, or if there're any other reasons for them to fail? One of the failing proofs, e.g., is erc20/hkg/balanceOf-spec.k, which seems to have no label.

[tothtamas28]

this PR is failing on erc20 tests starting from pyk version 0.1.616

I looked into this, and I think it's not pyk v0.1.616 that's causing the issue but this PR: #2243.

Below is the process I followed.

Setup

• Identify what's failing on CI. Some Booster tests are failing, I picked one: erc20/hkg/transferFrom-failure-2-spec.k.

• Reproduce locally with pytest:

  make test-integration PYTEST_ARGS='-n0 -k transferFrom-failure-2-spec -vvv'
  

• Reproduce locally without pytest, i.e. with kevm commands:

  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')))),))

Identifying root cause

• Configuration kevm-pyk v1.0.447 / pyk v0.1.616 / K v6.2.4 is known to be failing.

• pyk v0.1.606 effectively disabled the failing test, so I looked for the last successful CI run before integrating that version. It was on ceec292. The corresponding configuration is kevm-pyk v1.0.433 / pyk v0.1.605 / K v6.1.104. That configuration passes locally as well.

• pyk v0.1.616 re-enabled this test, so I bumped versions to the most recent ones: pyk v0.1.618 / K v6.2.4. The test still passes. This rules out pyk and K as the culprit.

• I started bisecting kevm-pyk versions between v1.0.433 and v1.0.447 using pyk v0.1.618 / K v6.2.4. The first one failing is v1.0.446.

[palinatolmach]

@tothtamas28 thanks a lot for the investigation! Then, if I understand correctly, one of always_check_subsumption, fast_check_subsumption, post_exec_simplify being on by default since #2243 probably causes these tests to fail. I'll try to find which one exactly.

[palinatolmach]

Update: based on my local experiments, setting fast_check_subsumption to False by default makes tests pass:

evm-semantics/kevm-pyk/src/kevm_pyk/__main__.py

Line 302 in 5d6d9b6

fast_check_subsumption: bool = True,

@tothtamas28 can I ask for your advice on what's best to do in this situation? Is it ok for me to push this change to this PR (for engagement unblocking purposes) and submit an issue so we can investigate it further afterwards?

[tothtamas28]

Is it ok for me to push this change to this PR (for engagement unblocking purposes) and submit an issue so we can investigate it further afterwards?

Yes, that sounds like the best strategy in this case.

[ehildenb]

@palinatolmach @tothtamas28 @anvacaru let's make sure when we switch a CLI option like this one, we also switch the default in cli.py as well to match it

evm-semantics/kevm-pyk/src/kevm_pyk/cli.py

Line 70 in 9e88278

args.add_argument(

[tothtamas28]

Possibly related: runtimeverification/kontrol#298 (review)

[palinatolmach]

Right, thanks! I created an issue so that I don't forget to address it within the next few days: #2295, and I'll check with @nwatson22 on whether we might incorporate runtimeverification/kontrol#298 (review) in fixing that as well.