Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/k_release
Original file line number Diff line number Diff line change
@@ -1 +1 @@
7.1.244
7.1.249
16 changes: 8 additions & 8 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
description = "A flake for the KEVM Semantics";

inputs = {
k-framework.url = "github:runtimeverification/k/v7.1.244";
k-framework.url = "github:runtimeverification/k/v7.1.249";
nixpkgs.follows = "k-framework/nixpkgs";
flake-utils.follows = "k-framework/flake-utils";
rv-utils.follows = "k-framework/rv-utils";
Expand Down
105 changes: 11 additions & 94 deletions kevm-pyk/poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ authors = [
[tool.poetry.dependencies]
python = "^3.10"
pathos = "*"
kframework = "7.1.244"
kframework = "7.1.249"
tomlkit = "^0.11.6"
frozendict = "^2.4.6"

Expand Down
10 changes: 5 additions & 5 deletions kevm-pyk/src/kevm_pyk/kevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -20,17 +20,17 @@
top_down,
)
from pyk.kast.manip import abstract_term_safely, flatten_label, set_cell
from pyk.kast.prelude.bytes import BYTES, pretty_bytes
from pyk.kast.prelude.kint import INT, gtInt, intToken, ltInt
from pyk.kast.prelude.ml import mlEqualsFalse, mlEqualsTrue
from pyk.kast.prelude.string import stringToken
from pyk.kast.prelude.utils import token
from pyk.kast.pretty import paren
from pyk.kcfg.kcfg import KCFGExtendResult, Step
from pyk.kcfg.semantics import DefaultSemantics
from pyk.kcfg.show import NodePrinter
from pyk.ktool.kprove import KProve
from pyk.ktool.krun import KRun
from pyk.prelude.bytes import BYTES, pretty_bytes
from pyk.prelude.kint import INT, gtInt, intToken, ltInt
from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue
from pyk.prelude.string import stringToken
from pyk.prelude.utils import token
from pyk.proof.reachability import APRProof
from pyk.proof.show import APRProofNodePrinter

Expand Down
8 changes: 4 additions & 4 deletions kevm-pyk/src/kevm_pyk/summarizer.py
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@
from pyk.kast.att import Atts
from pyk.kast.inner import KApply, KRewrite, KSequence, KToken, KVariable, Subst, top_down
from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire, KRule, KSort
from pyk.kast.prelude.k import DOTS
from pyk.kast.prelude.kbool import andBool
from pyk.kast.prelude.kint import addInt, eqInt, euclidModInt, leInt, ltInt
from pyk.kast.prelude.ml import mlEquals, mlEqualsFalse, mlEqualsTrue, mlNot
from pyk.kcfg import KCFG, KCFGExplore
from pyk.kdist import kdist
from pyk.kore.rpc import KoreClient
from pyk.prelude.k import DOTS
from pyk.prelude.kbool import andBool
from pyk.prelude.kint import addInt, eqInt, euclidModInt, leInt, ltInt
from pyk.prelude.ml import mlEquals, mlEqualsFalse, mlEqualsTrue, mlNot
from pyk.proof import APRProof
from pyk.proof.show import APRProofShow
from pyk.utils import ensure_dir_path
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/utils.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,11 @@
split_config_and_constraints,
split_config_from,
)
from pyk.kast.prelude.ml import is_bottom, is_top
from pyk.kcfg import KCFGExplore
from pyk.kore.rpc import KoreExecLogFormat
from pyk.ktool import TypeInferenceMode
from pyk.ktool.claim_loader import ClaimLoader
from pyk.prelude.ml import is_bottom, is_top
from pyk.proof import APRProof, APRProver
from pyk.proof.implies import EqualityProof, ImpliesProver
from pyk.proof.proof import parallel_advance_proof
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/tests/unit/test_kevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@

from pyk.cterm.cterm import CTerm
from pyk.kast.inner import KApply, KToken, KVariable
from pyk.prelude.utils import token
from pyk.kast.prelude.utils import token

from kevm_pyk.kevm import KEVM, KEVMSemantics, compute_jumpdests

Expand Down
Loading