diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 703ec070dc..aadd258538 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -132,13 +132,13 @@ jobs: include: - test-suite: 'test-prove-kprove' test-args: - timeout: 90 + timeout: 45 - test-suite: 'test-prove-pyk' test-args: - timeout: 90 + timeout: 120 - test-suite: 'test-prove-pyk' test-args: '--use-booster' - timeout: 60 + timeout: 90 timeout-minutes: ${{ matrix.timeout }} steps: - name: 'Check out code' @@ -170,7 +170,7 @@ jobs: include: - test-suite: 'legacy' test-args: - timeout: 240 + timeout: 180 - test-suite: 'booster' test-args: '--use-booster' timeout: 90 diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 5a9be299e8..0540edcf4b 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.302" +version = "1.0.303" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 3f728a5db9..ef4ed549fe 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.302' +VERSION: Final = '1.0.303' diff --git a/package/version b/package/version index 9667f83861..da86f30c3b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.302 +1.0.303 diff --git a/tests/failing-symbolic.haskell b/tests/failing-symbolic.haskell index 695cdb044d..a8977a731a 100644 --- a/tests/failing-symbolic.haskell +++ b/tests/failing-symbolic.haskell @@ -1,39 +1,120 @@ +tests/specs/benchmarks/address00-spec.k +tests/specs/benchmarks/bytes00-spec.k +tests/specs/benchmarks/ecrecover00-siginvalid-spec.k +tests/specs/benchmarks/ecrecover00-sigvalid-spec.k 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/encode-keccak00-spec.k +tests/specs/benchmarks/encodepacked-keccak01-spec.k +tests/specs/benchmarks/functional-spec.k +tests/specs/benchmarks/keccak00-spec.k +tests/specs/benchmarks/overflow00-nooverflow-spec.k +tests/specs/benchmarks/overflow00-overflow-spec.k +tests/specs/benchmarks/requires01-a0gt0-spec.k +tests/specs/benchmarks/requires01-a0le0-spec.k +tests/specs/benchmarks/staticarray00-spec.k +tests/specs/benchmarks/staticloop00-a0lt10-spec.k +tests/specs/benchmarks/storagevar00-spec.k +tests/specs/benchmarks/storagevar01-spec.k +tests/specs/benchmarks/storagevar02-nooverflow-spec.k +tests/specs/benchmarks/storagevar02-overflow-spec.k +tests/specs/benchmarks/storagevar03-spec.k tests/specs/bihu/collectToken-spec.k +tests/specs/bihu/forwardToHotWallet-failure-1-spec.k +tests/specs/bihu/forwardToHotWallet-failure-2-spec.k +tests/specs/bihu/forwardToHotWallet-failure-3-spec.k +tests/specs/bihu/forwardToHotWallet-failure-4-spec.k +tests/specs/bihu/forwardToHotWallet-success-1-spec.k +tests/specs/bihu/forwardToHotWallet-success-2-spec.k +tests/specs/bihu/functional-spec.k +tests/specs/erc20/ds/allowance-spec.k +tests/specs/erc20/ds/approve-failure-spec.k +tests/specs/erc20/ds/approve-success-spec.k +tests/specs/erc20/ds/balanceOf-spec.k +tests/specs/erc20/ds/totalSupply-spec.k +tests/specs/erc20/ds/transfer-failure-1-a-spec.k tests/specs/erc20/ds/transfer-failure-1-b-spec.k +tests/specs/erc20/ds/transfer-failure-1-c-spec.k +tests/specs/erc20/ds/transfer-failure-2-a-spec.k +tests/specs/erc20/ds/transfer-failure-2-b-spec.k tests/specs/erc20/ds/transferFrom-failure-1-a-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-failure-1-d-spec.k +tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k +tests/specs/erc20/ds/transferFrom-failure-2-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/erc20/ds/transfer-success-2-spec.k +tests/specs/erc20/hkg/allowance-spec.k +tests/specs/erc20/hkg/approve-spec.k +tests/specs/erc20/hkg/balanceOf-spec.k +tests/specs/erc20/hkg/totalSupply-spec.k +tests/specs/erc20/hkg/transfer-failure-1-spec.k +tests/specs/erc20/hkg/transfer-failure-2-spec.k +tests/specs/erc20/hkg/transferFrom-failure-1-spec.k +tests/specs/erc20/hkg/transferFrom-failure-2-spec.k tests/specs/erc20/hkg/transferFrom-success-1-spec.k +tests/specs/erc20/hkg/transferFrom-success-2-spec.k +tests/specs/erc20/hkg/transfer-success-1-spec.k +tests/specs/erc20/hkg/transfer-success-2-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/functional/evm-int-simplifications-spec.k +tests/specs/functional/infinite-gas-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 +tests/specs/mcd/dai-adduu-fail-rough-spec.k +tests/specs/mcd/dai-symbol-pass-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/dsvalue-peek-pass-rough-spec.k +tests/specs/mcd/dsvalue-read-pass-spec.k +tests/specs/mcd/dsvalue-read-pass-summarize-spec.k tests/specs/mcd/end-cash-pass-rough-spec.k tests/specs/mcd/end-pack-pass-rough-spec.k +tests/specs/mcd/end-subuu-pass-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-addu48u48-fail-rough-spec.k tests/specs/mcd/flipper-bids-pass-rough-spec.k +tests/specs/mcd/flipper-tau-pass-spec.k +tests/specs/mcd/flipper-ttl-pass-spec.k +tests/specs/mcd/flopper-cage-pass-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-fail-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-mului-pass-spec.k +tests/specs/mcd/vat-muluu-pass-spec.k tests/specs/mcd/vat-slip-pass-rough-spec.k +tests/specs/mcd/vat-subui-fail-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/opcodes/create-spec.k diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index ad74273a6b..14bd7d5a93 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -5,51 +5,7 @@ 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/benchmarks/staticarray00-spec.k -tests/specs/benchmarks/staticloop00-a0lt10-spec.k -tests/specs/benchmarks/storagevar00-spec.k -tests/specs/benchmarks/storagevar01-spec.k -tests/specs/benchmarks/storagevar02-nooverflow-spec.k -tests/specs/benchmarks/storagevar02-overflow-spec.k tests/specs/bihu/collectToken-spec.k -tests/specs/bihu/forwardToHotWallet-failure-1-spec.k -tests/specs/bihu/forwardToHotWallet-failure-3-spec.k -tests/specs/bihu/forwardToHotWallet-failure-4-spec.k -tests/specs/bihu/forwardToHotWallet-success-1-spec.k -tests/specs/bihu/forwardToHotWallet-success-2-spec.k -tests/specs/erc20/ds/allowance-spec.k -tests/specs/erc20/ds/approve-failure-spec.k -tests/specs/erc20/ds/approve-success-spec.k -tests/specs/erc20/ds/balanceOf-spec.k -tests/specs/erc20/ds/totalSupply-spec.k -tests/specs/erc20/ds/transfer-failure-1-a-spec.k -tests/specs/erc20/ds/transfer-failure-1-b-spec.k -tests/specs/erc20/ds/transfer-failure-1-c-spec.k -tests/specs/erc20/ds/transfer-failure-2-a-spec.k -tests/specs/erc20/ds/transfer-failure-2-b-spec.k -tests/specs/erc20/ds/transferFrom-failure-1-a-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-failure-1-d-spec.k -tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k -tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k -tests/specs/erc20/ds/transferFrom-failure-2-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/erc20/ds/transfer-success-2-spec.k -tests/specs/erc20/hkg/allowance-spec.k -tests/specs/erc20/hkg/approve-spec.k -tests/specs/erc20/hkg/balanceOf-spec.k -tests/specs/erc20/hkg/totalSupply-spec.k -tests/specs/erc20/hkg/transfer-failure-1-spec.k -tests/specs/erc20/hkg/transfer-failure-2-spec.k -tests/specs/erc20/hkg/transferFrom-failure-1-spec.k -tests/specs/erc20/hkg/transferFrom-failure-2-spec.k -tests/specs/erc20/hkg/transferFrom-success-1-spec.k -tests/specs/erc20/hkg/transferFrom-success-2-spec.k -tests/specs/erc20/hkg/transfer-success-1-spec.k -tests/specs/erc20/hkg/transfer-success-2-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 @@ -65,14 +21,8 @@ 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-addu48u48-fail-rough-spec.k -tests/specs/mcd/flipper-bids-pass-rough-spec.k -tests/specs/mcd/flipper-tau-pass-spec.k -tests/specs/mcd/flipper-ttl-pass-spec.k -tests/specs/mcd/flopper-cage-pass-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/gemjoin-exit-pass-rough-spec.k diff --git a/tests/failing-symbolic.pyk b/tests/failing-symbolic.pyk index f049eedfd9..bc3f33fb71 100644 --- a/tests/failing-symbolic.pyk +++ b/tests/failing-symbolic.pyk @@ -1,4 +1,3 @@ -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 @@ -6,29 +5,8 @@ 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/bihu/forwardToHotWallet-failure-1-spec.k -tests/specs/bihu/forwardToHotWallet-failure-3-spec.k -tests/specs/bihu/forwardToHotWallet-failure-4-spec.k -tests/specs/bihu/forwardToHotWallet-success-1-spec.k -tests/specs/bihu/forwardToHotWallet-success-2-spec.k -tests/specs/erc20/ds/transfer-failure-1-b-spec.k -tests/specs/erc20/ds/transferFrom-failure-1-a-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-failure-1-d-spec.k -tests/specs/erc20/ds/transferFrom-failure-2-a-spec.k -tests/specs/erc20/ds/transferFrom-failure-2-b-spec.k -tests/specs/erc20/ds/transferFrom-failure-2-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/erc20/hkg/approve-spec.k -tests/specs/erc20/hkg/transferFrom-failure-1-spec.k -tests/specs/erc20/hkg/transferFrom-failure-2-spec.k -tests/specs/erc20/hkg/transferFrom-success-1-spec.k -tests/specs/erc20/hkg/transferFrom-success-2-spec.k -tests/specs/erc20/hkg/transfer-success-1-spec.k -tests/specs/erc20/hkg/transfer-success-2-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 @@ -43,7 +21,6 @@ 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