-
Notifications
You must be signed in to change notification settings - Fork 147
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Cleanup failing lists, enable more failing tests (#2067)
* tests/failing-symbolic.pyk: remove now passing tests
* tests/failing-symbolic.haskell-booster: remove now passing tests
* tests/failing-symbolic.haskell-booster: update failing list
* tests/failing-symbolic.pyk: update failing list
* tests/failing-symbolic.{haskell-booster,pyk}: re-disable int-simplifications file
* tests/specs/functional/int-simplifications: remove runLemma => doneLemma indirection
* Revert "tests/specs/functional/int-simplifications: remove runLemma => doneLemma indirection"
This reverts commit 18e1f149ca2c41c4baeee7ad5ab73b38694945e6.
* tests/specs/functional/lemmas-spec: remove runLemma => doneLemma style claims
* Revert "tests/specs/functional/lemmas-spec: remove runLemma => doneLemma style claims"
This reverts commit d2d5c659cd9b96d038794da5de8f0656e7d87e59.
* tests/specs/functional/merkle-spec: remove indirectoin of runLemma => doneLemma
* Revert "tests/specs/functional/merkle-spec: remove indirectoin of runLemma => doneLemma"
This reverts commit 2aae1cad0b5ed0a00c1d875c2646da4d3f7b224e.
* tests/specs/functional/storageRoot-spec.k: remove indirection of runLemma => doneLemma specs
* Revert "tests/specs/functional/storageRoot-spec.k: remove indirection of runLemma => doneLemma specs"
This reverts commit 1692b593435c8ac0aa3a9de79af80680ab7b8e43.
* tests/specs/benchmarks/functional-spec: remove runLemma => doneLemma claim stuffs
* Revert "tests/specs/benchmarks/functional-spec: remove runLemma => doneLemma claim stuffs"
This reverts commit d64eac1407116b3c52e6be3c77608bef1447f3ce.
* tests/failing-symbolic.{pyk,haskell-booster}: add back tests failing on RPC server
* tests/failing-symbolic.haskell: skip tests on kprove backend that are running on RPC backend
* tests/failing-symbolic.haskell-booster: add tests which are failing
* Set Version: 1.0.301
* tests/failing-symbolic.{pyk,haskell-booster,haskell}: disable tests taking longer than 900s
* .github/test-pr: adjust timeouts
* .github/test-pr: update timeout
* Set Version: 1.0.302
* tests/failing-symbolic.haskell: disable long-running tests
* .github/test-pr: udpate timeouts
* Set Version: 1.0.303
---------
Co-authored-by: devops <[email protected]>- Loading branch information
Showing
7 changed files
with
88 additions
and
80 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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. <[email protected]>", | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -6,4 +6,4 @@ | |
| from typing import Final | ||
|
|
||
|
|
||
| VERSION: Final = '1.0.302' | ||
| VERSION: Final = '1.0.303' | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1 +1 @@ | ||
| 1.0.302 | ||
| 1.0.303 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters