Rebase onto recent version of upstream #9
Conversation
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
* add attributes for the haskell backend * separate lemma modules for java backend and haskell backend * remove unnecessary lemmas * fix typo
* prove hkg-totalSupply using haskell backend * add #gas declaration in the VERIFICATION-HASKELL module * move defineness axiom for #buf
* web3.md: add revert reason to error msg * fix test output
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * tests/interactive/search: update expected output Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
* state-loader: formatting * json: add some documentation * json: add JSON sorting infra * json: add +JSONs and use it in qsortJSONs * driver: switch to library versions of JSON handling * json, data, serialization: separate out JSON and JSON-EXT modules * json: use JSONKey as subsort of JSON to avoid least sort calculation issue * json: fix bug in qsort algorithm
* specs.md: added assertEq * specs.md: added #mkCallShortcut * specs.md: slightly generalized #assume, #assert - added ==S strict equality Exp. * specs.md: re-added regular rule for #assert. Spec rule doesnt work. * specs.md: #assert corrected * specs.md: extended expression language for specifying `ensures` * specs.md: KEVM main module for for SOLAR-style specs * Makefile: support for SOLAR module compilation * specs.md: added #getRefund * specs.md: renamed getVar to #var() * specs.md: reorganized, refactored, added more config access * specs.md: added +List * specs: cleanup * evm-imp-specs: formatting * evm-imp-specs.md: renamed, PR comments addressed * Makefile: renamed, make sure we remain compatible with cmake build system (+2 squashed commit) * solar: fixed transition to ByteArray * solar: unit tests * solar: unit tests. Multiple fixes. Looks like a lemma is missing. * solar: finished unit tests * solar: renaming all "solar" to "imp-specs" * Makefile: formatting Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* deps/plugin: update submodule * Revert "Update dependency: deps/plugin (runtimeverification#740)" Co-authored-by: Andrei <andrei.vacaru@runtimeverification.com>
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: 96e9ad963 - remove remaining instances of kil.Attribute and kil.Attributes classes (runtimeverification#1153) * tests/specs/benchmarks: clean up import structure slightly * tests/specs/functional/merkle-spec: correctly existentially bind variables on RHS of claim Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
…erification#755) * use pipe instead of socket in web3.md * remove some unnecessary brackets that z3 doesn't like * don't pass --kport to kevm-client * tmp: update submodule * fix formatting * Makefile: do not prefix commands with K_BIN (runtimeverification#756) * deps/plugin: 92bc7a0 - use pipes instead of a socket for communication with K (runtimeverification#91) Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* Simplification rules for bool2Word The Haskell backend will use these simplification rules to simplify the common patterns `bool2Word(B) ==Int 0` and `bool2Word(B) ==Int 1` to fix a performance regression. Previously, the frontend emitted rules that generalized `==Int` to `==K`. Then, the backend would branch on `==K`. However, branching causes other performance problems, so the simplification rules seem like a good compromise. * sum-to-n-spec: Import LEMMAS Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule
* deps/k: update submodule * deps/k: update submodule
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule
* web3.md: Handle null argument for eth_getBlockByNumber * state-loader,web3: Handle integer argument for parsing block identifiers
* WIP: add lemmas and test * Finish adding lemmas and tests * Revert change * Update tests/specs/functional/lemmas-spec.k Co-Authored-By: ehildenb <everett.hildenbrandt@gmail.com> * Separate lemmas-spec + run without smt Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* Size related lemmas * Add simplification rule for minInt * klabel and smtlib for #sizeByteArray. * Fix formatting. * Remove lemmas that do not work with the Java backend * smtlib attribute for all versions of #sizeByteArray * evm, evm-types: merge issues * Makefile, tests/specs/functional/lemmas-spec: working lemmas on Haskell backend * tests/specs/lemmas: add range access simplification lemmas * tests/specs/lemmas: remove uneeded lemma Co-authored-by: Virgil Serbanuta <virgil.serbanuta> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
* Jenkinsfile: formatting * Jenkinsfile: add back Jello Paper deploy stage * !!! Jenkinsfile: debugging * Jenkinsfile: correct close braces * Jenkinsfile: handle cloning evm-semantics directly in sh script * Revert "!!! Jenkinsfile: debugging" * Jenkinsfile: stage name
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule
* web3.md: refactor finishTX * change <errorPC> to <endPC> * update specs * Update web3.md: formatting * update tests * update more tests * evm.md: don't store <endPC> for VMTESTS execmode * Revert "evm.md: don't store <endPC> for VMTESTS execmode" This reverts commit 5f22e47. * driver: clear endPC cell on success Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* tests/failing: remove failing VMTests
* tests/slow: remove slow VMTests
* tests/: update slow/failing lists
* tests/slow.haskell: limit to 15s or less
* tests/slow.haskell: add everything above the first 100 tests
* tests/{slow,failing}.haskell: reset lists
* tests/slow: strict removal of <15s tests
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
* implement firefly_setGasPrice * update tests * update tests * add defaultGas cells * update test file * update tests output * web3.md: add makeTx * Web3.md: simplify rule
* README: Update repository layout * README: ordering/formatting Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule
* web3.md: firefly_setNetworkId * formatting * add test
* web3: Update blockhashes cell on #pushBlockchainState
* web3: use structural framing instead of dont care
* web3: Update blockhashes cell on #popNetworkState
* web3: Increment block number after mining (off by one for BLOCKHASH instruction)
* web3: pending block = latest block (mimics ganache)
* web3: Make transaction receipts when mining
* tests/web3/blockhashes: Add test for BLOCKHASH instruction
* tests/web3/sendRawTransaction{2,_noTo}: Create genesis block on tests involving blocks
* tests/failing.web3: blockhashes should work
Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
…n#777) * evm-types: make _[_.._] total * evm-types: mark #range as total now too * tests/specs/functional/lemmas-spec: enable commented out proof * evm-types: make sure both START and WIDTH are greater than 0 * evm-types: formatting
* deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule * deps/k: update submodule Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* tests/web3/sendRawTransaction_non27or28_V: Add test for transactions with alternate signing method * serialization.md: Add alternate way to hash transaction for signing * web3: Implement address recovery for alternately signed transactions * serialization: Add #sender helper for alternately signed transactions * serialization: Expand new #sender to handle both signing cases * driver/web3: Make any use of #sender the new one * serialization: Remove old #sender * web3: eth_sendRawTransactionVerify: Remove double rule Co-authored-by: rv-jenkins <admin@runtimeverification.com>
… (runtimeverification#779) Co-authored-by: ehildenb <everett.hildenbrandt@gmail.com>
* kevm: add use --ip flag in run_web3 function * kevm: fix typo * deps/plugin: fbce972 - main.cpp: remove duplicated flag (runtimeverification#93) Co-authored-by: Andrei <andrei.vacaru@runtimeverification.com>
…timeverification#778) * web3: Ignore unknown fields in loadTransaction * web3: Formatting Co-authored-by: rv-jenkins <admin@runtimeverification.com>
* deps/k: fdc13d071 - add a proof example for arrays (runtimeverification#1242) * deps/k: 38c719288 - Packaging subdirectory [brew-staging: directory-change] (runtimeverification#1227) * deps/k: 2fcdb581e - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1240) * deps/k: 371c4764b - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1245)
* deps/k: a235afa15 - Dockerhub images (runtimeverification#1228) * deps/k: 3bfd4f805 - java-backend: improve smt query log formatting (runtimeverification#1248)
* Makefile, README, cmake/node: remove node build from semantics * Dockerfile, README, package/*: remove protobuf dependencies * driver, evm-node: remove node instrumentation * evm, driver: remove #loadAccount, #lookupCode, and #lookupStorage * evm: use owise rule instead of direct boolean * evm: inline #addr? and #code? * evm: remove useless rules * evm: rename #load => #addr * evm: remove owise from non-function rule
* deps/k: 8e62798b6 - llvm-backend/src/main/native/llvm-backend: fa4c44f - fix non-exhaustiveness bug (runtimeverification#324) (runtimeverification#1253) * deps/k: 4a011c920 - haskell-backend/src/main/native/haskell-backend: b3c17111 - Fix sorting bugs around RulePattern (runtimeverification#1787) (runtimeverification#1251)
* deps/plugin: 42d31c1 - Remove obsolete files (runtimeverification#95) * cmake/client: adjust for new location of init files Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
* web3: Make timestamp more dynamic and have better support for custom values * web3: rename lastMineTime cell to lastTime * web3: Keep a time adjustment instead of tracking last update * web3: Update timestamp just before executing transactions instead of after mining (realtime accuracy) * web3: update timestamp on evm_mine * tests/web3: Fix tests broken by timestamp changes * tests/web3: Add failing test for evm_increaseTime Co-authored-by: rv-jenkins <admin@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
* specs/lemmas.k: extracted some lemmas common to Java and Haskell to common module. Required for symbolic testing. * evm-types: #lookup: marking [functional]. Sound change. * lemmas: extra lemma for byte array simplification (+1 squashed commits) Squashed commits: [ca5056a] lemmas.k: extra for kore and symb-testing. * symb-test: evm-types: Yi changes * edsl,evm-types,serialization: extensions for symb-test * edsl: small refactoring for symb-test * formatting fixes * Revert "symb-test: evm-types: Yi changes" This reverts commit 8682019. * evm-types, edsl: replacing some [functional] with #Ceil rules * formatting fixes * evm-types: One more #Ceil rule * evm-types: #Ceil rule correction * evm-types: replaced [functional] with #Ceil for #lookup * lemmas: PR comments addressed * evm-types: moved all #Ceil rules in one place, to be compatible with all backends. * PR fixes * PR fix - #Ceil(#buf) rule generates condition for SIZE and DATA * symb-test: #Ceil rules for #padToWidth, #patRightToWidth corrected. * symb-test: reverting rule #Ceil(#buf(SIZE, DATA)) to simplified form for performance reasons. * evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related rules. * lemmas.k: [..] rule simplified * lemmas.k: #sizeWordStack rule side conditions * erc20/abstract-semantics-segmented-gas.k: dependency removed * fix for previous * evm-types: removed #Ceil rules for padLeftBytes, padRightBytes. Moved to k/domains.k * edsl: Full #Ceil rule for #buf, but slow for erc20-verifier. * evm-types: replaced 3 `#Ceil` rules with complete definition and [functional] * Reverse commit "evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related rules" * formatting * evm: performance enhancement driven by profiling ERC20 specs. * Makefile: added tangle mode `symbolic-bytes` just for Haskell backend. * evm-types: fixes * evm-types: make #padToWidth and #padRightToWidth total * evm-types: leave wordstack alone if negative update is provided * evm: formatting * Reverse commit "Makefile: added tangle mode `symbolic-bytes` just for Haskell backend." Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
* deps/k: fae525873 - GLR Bison parser (runtimeverification#1247) * deps/k: db11f1fa3 - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1261) * deps/k: 19747bbd3 - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1266) * deps/k: ec708d7e6 - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1274)
* initial test * format * draft test * add test to failing list * short test * wip * tests/web3/arbRollup: Raw rpc logs for arbRollup test * tests/web3/arbRollup: Minimize as best as possible * tests/failing.web3: arbRollup fixed by timestamp updates Co-authored-by: Guy Repta <50716988+gtrepta@users.noreply.github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>
…tion#794) * edsl: #Ceil(#buf) rule transformed from ^Int to <<Int. Possibly faster. * attribute fix * simplified Co-authored-by: rv-jenkins <admin@runtimeverification.com>
…ation#801) * Makefile: make explicit variable LOCAL_LIB * Makefile: remove unused variables INSTALL_PREFIX and INSTALL_DIR * Makefile: set K_RELEASE based on where K is * Makefile: remove git submodule updates * Makefile: remove redundant K_RELEASE setting * Makefile: remove split-tests target * Jenkinsfile: remove split-tests stage * Makefile: formatting * Makefile: factor out STANDALONE_KOMPILE_OPTS * Makefile: formatting * Makefile: remove duplicate -I $(llvm_dir) * Makefile, README: remove LIBFF_CC and LIBFF_CXX * Makefile: set K_RELEASE with abspath for cmake * cmake/client/CMakeLists: allow for global install of K too * Makefile: organize * Makefile: depend directly on files in submodules * kevm: same logic for setting K_RELEASE * Makefile: remove PKG_CONFIG_PATH variable * Makefile: correct depending on K Jar * README: update instructions * Makefile: add include/kllvm to STANDALONE_KOMPILE_OPTS * Jenkinsfile: increase parallelism of build step * Makefile: full path to K_LIB
* deps/k: f53775989 - Reorganize K distribution to remove dependence on /usr/lib/kframework sysroot [brew-staging: reorg] (runtimeverification#1272) * deps/k: 49b27fdb5 - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1297) * deps/k: b0845f74c - Changes to K frontend to support new C++ unparsing (runtimeverification#1287) * deps/k: 4201087d8 - Adding support for .md files (runtimeverification#1116) * deps/k: a2f6e8b76 - fix AddEmptyList for --bison-lists (runtimeverification#1298) * deps/k: b35c36e97 - Update dependency: haskell-backend/src/main/native/haskell-backend (runtimeverification#1301) * deps/k: 5396aae9a - A few minor features (runtimeverification#1304)
|
dapphub/klab#422 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Tested
klabwith this rebased repo; all example proofs accept. Also tested all proofs in this repo.If more testing is desired: here is a
klabthat points itsevm-semanticsat the proposed changes.