From d5dc5262bfd14182f1cf593693bccaf52218890c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 8 Feb 2024 18:01:09 +0000 Subject: [PATCH 1/6] !!! tests/failing: enable all the tests --- tests/failing-symbolic.haskell-booster | 38 -------------------- tests/failing-symbolic.pyk | 48 -------------------------- 2 files changed, 86 deletions(-) diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index 6cc20db2ad..7ae58589e0 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -1,39 +1 @@ -tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k -tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k -tests/specs/benchmarks/functional-spec.k -tests/specs/bihu/collectToken-spec.k -tests/specs/examples/erc721-spec.md -tests/specs/examples/sum-to-n-foundry-spec.k -tests/specs/examples/sum-to-n-spec.k -tests/specs/functional/infinite-gas-spec.k -tests/specs/functional/int-simplifications-spec.k -tests/specs/functional/lemmas-no-smt-spec.k -tests/specs/functional/lemmas-spec.k -tests/specs/functional/merkle-spec.k -tests/specs/functional/storageRoot-spec.k -tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k -tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k -tests/specs/mcd/end-cash-pass-rough-spec.k -tests/specs/mcd/end-pack-pass-rough-spec.k -tests/specs/mcd/flapper-tend-guy-diff-pass-rough-spec.k -tests/specs/mcd/flapper-yank-pass-rough-spec.k -tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k -tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k -tests/specs/mcd/flopper-kick-pass-rough-spec.k -tests/specs/mcd/flopper-tick-pass-rough-spec.k -tests/specs/mcd/gemjoin-exit-pass-rough-spec.k -tests/specs/mcd/pot-join-pass-rough-spec.k -tests/specs/mcd/vat-flux-diff-pass-rough-spec.k -tests/specs/mcd/vat-fold-pass-rough-spec.k -tests/specs/mcd/vat-fork-diff-pass-rough-spec.k -tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k -tests/specs/mcd/vow-cage-deficit-pass-rough-spec.k -tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k -tests/specs/mcd/vow-fess-fail-rough-spec.k -tests/specs/mcd/vow-flog-fail-rough-spec.k tests/specs/opcodes/create-spec.k -tests/specs/opcodes/evm-optimizations-spec.md diff --git a/tests/failing-symbolic.pyk b/tests/failing-symbolic.pyk index 49ef633baf..7ae58589e0 100644 --- a/tests/failing-symbolic.pyk +++ b/tests/failing-symbolic.pyk @@ -1,49 +1 @@ -tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k -tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k -tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k -tests/specs/benchmarks/functional-spec.k -tests/specs/bihu/collectToken-spec.k -tests/specs/erc20/ds/transfer-failure-1-b-spec.k -tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k -tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k -tests/specs/erc20/ds/transferFrom-success-1-spec.k -tests/specs/erc20/ds/transferFrom-success-2-spec.k -tests/specs/erc20/ds/transfer-success-1-spec.k -tests/specs/examples/erc20-spec.md -tests/specs/examples/erc721-spec.md -tests/specs/examples/sum-to-n-foundry-spec.k -tests/specs/examples/sum-to-n-spec.k -tests/specs/functional/int-simplifications-spec.k -tests/specs/functional/lemmas-no-smt-spec.k -tests/specs/functional/lemmas-spec.k -tests/specs/functional/merkle-spec.k -tests/specs/functional/storageRoot-spec.k -tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k -tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k -tests/specs/mcd/end-cash-pass-rough-spec.k -tests/specs/mcd/end-pack-pass-rough-spec.k -tests/specs/mcd/flapper-tend-guy-diff-pass-rough-spec.k -tests/specs/mcd/flapper-yank-pass-rough-spec.k -tests/specs/mcd/flipper-bids-pass-rough-spec.k -tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k -tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k -tests/specs/mcd/flopper-file-pass-rough-spec.k -tests/specs/mcd/flopper-kick-pass-rough-spec.k -tests/specs/mcd/flopper-tick-pass-rough-spec.k -tests/specs/mcd/functional-spec.k -tests/specs/mcd/gemjoin-exit-pass-rough-spec.k -tests/specs/mcd/pot-join-pass-rough-spec.k -tests/specs/mcd/vat-flux-diff-pass-rough-spec.k -tests/specs/mcd/vat-fold-pass-rough-spec.k -tests/specs/mcd/vat-fork-diff-pass-rough-spec.k -tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k -tests/specs/mcd/vat-move-diff-rough-spec.k -tests/specs/mcd/vat-slip-pass-rough-spec.k -tests/specs/mcd/vow-cage-deficit-pass-rough-spec.k -tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k -tests/specs/mcd/vow-fess-fail-rough-spec.k -tests/specs/mcd/vow-flog-fail-rough-spec.k tests/specs/opcodes/create-spec.k -tests/specs/opcodes/evm-optimizations-spec.md From 54a2aaa9dc8683def147d74a5ec80e3f6fccacf0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Feb 2024 15:29:16 +0000 Subject: [PATCH 2/6] tests/failing-symbolic.haskell-booster: disable failing tests --- tests/failing-symbolic.haskell-booster | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index 7ae58589e0..65da40d410 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -1 +1,21 @@ +tests/specs/bihu/collectToken-spec.k +tests/specs/examples/erc721-spec.md +tests/specs/examples/sum-to-n-foundry-spec.k +tests/specs/functional/int-simplifications-spec.k +tests/specs/functional/lemmas-no-smt-spec.k +tests/specs/functional/lemmas-spec.k +tests/specs/functional/storageRoot-spec.k +tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k +tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k +tests/specs/mcd/end-cash-pass-rough-spec.k +tests/specs/mcd/end-pack-pass-rough-spec.k +tests/specs/mcd/flapper-tend-guy-diff-pass-rough-spec.k +tests/specs/mcd/flapper-yank-pass-rough-spec.k +tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k +tests/specs/mcd/gemjoin-exit-pass-rough-spec.k +tests/specs/mcd/pot-join-pass-rough-spec.k +tests/specs/mcd/vat-fold-pass-rough-spec.k +tests/specs/mcd/vat-fork-diff-pass-rough-spec.k +tests/specs/mcd/vow-cage-deficit-pass-rough-spec.k +tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k tests/specs/opcodes/create-spec.k From 6f233718915607a1c068ecc4cb6322ee4a4be891 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Feb 2024 15:31:01 +0000 Subject: [PATCH 3/6] tests/failing-symbolic.pyk: disable failing and slow tests --- tests/failing-symbolic.pyk | 44 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/tests/failing-symbolic.pyk b/tests/failing-symbolic.pyk index 7ae58589e0..7b317e4634 100644 --- a/tests/failing-symbolic.pyk +++ b/tests/failing-symbolic.pyk @@ -1 +1,45 @@ +tests/specs/bihu/collectToken-spec.k +tests/specs/examples/erc20-spec.md +tests/specs/examples/erc721-spec.md +tests/specs/examples/solidity-code-spec.md +tests/specs/examples/storage-spec.md +tests/specs/examples/sum-to-n-foundry-spec.k +tests/specs/functional/infinite-gas-spec.k +tests/specs/functional/int-simplifications-spec.k +tests/specs/functional/lemmas-no-smt-spec.k +tests/specs/functional/lemmas-spec.k +tests/specs/functional/storageRoot-spec.k +tests/specs/mcd/cat-exhaustiveness-spec.k +tests/specs/mcd/cat-file-addr-pass-rough-spec.k +tests/specs/mcd/dstoken-approve-fail-rough-spec.k +tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k +tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k +tests/specs/mcd/end-cash-pass-rough-spec.k +tests/specs/mcd/end-pack-pass-rough-spec.k +tests/specs/mcd/flapper-tend-guy-diff-pass-rough-spec.k +tests/specs/mcd/flapper-yank-pass-rough-spec.k +tests/specs/mcd/flipper-bids-pass-rough-spec.k +tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k +tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k +tests/specs/mcd/flopper-file-pass-rough-spec.k +tests/specs/mcd/flopper-kick-pass-rough-spec.k +tests/specs/mcd/flopper-tick-pass-rough-spec.k +tests/specs/mcd/functional-spec.k +tests/specs/mcd/gemjoin-exit-pass-rough-spec.k +tests/specs/mcd/pot-join-pass-rough-spec.k +tests/specs/mcd/vat-addui-pass-spec.k +tests/specs/mcd/vat-deny-diff-fail-rough-spec.k +tests/specs/mcd/vat-flux-diff-pass-rough-spec.k +tests/specs/mcd/vat-fold-pass-rough-spec.k +tests/specs/mcd/vat-fork-diff-pass-rough-spec.k +tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k +tests/specs/mcd/vat-move-diff-rough-spec.k +tests/specs/mcd/vat-muluu-pass-spec.k +tests/specs/mcd/vat-slip-pass-rough-spec.k +tests/specs/mcd/vat-subui-pass-rough-spec.k +tests/specs/mcd/vat-subui-pass-spec.k +tests/specs/mcd/vow-cage-deficit-pass-rough-spec.k +tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k +tests/specs/mcd/vow-fess-fail-rough-spec.k +tests/specs/mcd/vow-flog-fail-rough-spec.k tests/specs/opcodes/create-spec.k From d97b2f657be3687bbf7f7e06d0b21415c1865fce Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Feb 2024 15:32:40 +0000 Subject: [PATCH 4/6] tests/failing-symbolic.pyk: disable previously disabled tests --- tests/failing-symbolic.pyk | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/tests/failing-symbolic.pyk b/tests/failing-symbolic.pyk index 7b317e4634..8acf9e0bab 100644 --- a/tests/failing-symbolic.pyk +++ b/tests/failing-symbolic.pyk @@ -1,13 +1,27 @@ +tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k +tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k +tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k +tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k +tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k +tests/specs/benchmarks/functional-spec.k tests/specs/bihu/collectToken-spec.k +tests/specs/erc20/ds/transfer-failure-1-b-spec.k +tests/specs/erc20/ds/transferFrom-failure-1-b-spec.k +tests/specs/erc20/ds/transferFrom-failure-1-c-spec.k +tests/specs/erc20/ds/transferFrom-success-1-spec.k +tests/specs/erc20/ds/transferFrom-success-2-spec.k +tests/specs/erc20/ds/transfer-success-1-spec.k tests/specs/examples/erc20-spec.md tests/specs/examples/erc721-spec.md tests/specs/examples/solidity-code-spec.md tests/specs/examples/storage-spec.md tests/specs/examples/sum-to-n-foundry-spec.k +tests/specs/examples/sum-to-n-spec.k tests/specs/functional/infinite-gas-spec.k tests/specs/functional/int-simplifications-spec.k tests/specs/functional/lemmas-no-smt-spec.k tests/specs/functional/lemmas-spec.k +tests/specs/functional/merkle-spec.k tests/specs/functional/storageRoot-spec.k tests/specs/mcd/cat-exhaustiveness-spec.k tests/specs/mcd/cat-file-addr-pass-rough-spec.k @@ -43,3 +57,4 @@ tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k tests/specs/mcd/vow-fess-fail-rough-spec.k tests/specs/mcd/vow-flog-fail-rough-spec.k tests/specs/opcodes/create-spec.k +tests/specs/opcodes/evm-optimizations-spec.md From f3fddbae481199781c5d980ffb57c70ec3fa8609 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Feb 2024 15:37:00 +0000 Subject: [PATCH 5/6] tests/failing-symbolic.haskell-booster: disable long-running tests --- tests/failing-symbolic.haskell-booster | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index 65da40d410..3536af751e 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -12,10 +12,12 @@ tests/specs/mcd/end-pack-pass-rough-spec.k tests/specs/mcd/flapper-tend-guy-diff-pass-rough-spec.k tests/specs/mcd/flapper-yank-pass-rough-spec.k tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k +tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k tests/specs/mcd/gemjoin-exit-pass-rough-spec.k tests/specs/mcd/pot-join-pass-rough-spec.k tests/specs/mcd/vat-fold-pass-rough-spec.k tests/specs/mcd/vat-fork-diff-pass-rough-spec.k +tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k tests/specs/mcd/vow-cage-deficit-pass-rough-spec.k tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k tests/specs/opcodes/create-spec.k From 51b7aaf0e5d2a03594e5a58922a9883245cc7dbb Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 Feb 2024 15:40:50 +0000 Subject: [PATCH 6/6] Set Version: 1.0.450 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 3adbe618c8..9f99ece121 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.449" +version = "1.0.450" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index ab0ca6c9b9..d8cdf46d25 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.449' +VERSION: Final = '1.0.450' diff --git a/package/version b/package/version index cc15fe6033..1e2d57a336 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.449 +1.0.450