Deleted PR #2645
Closed
Deleted PR #2645
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
This updates the CI to remove the checks that we no longer want to perform which are related to Nix or to the Haskell backend. --------- Co-authored-by: F-WRunTime <[email protected]>
Having this cell in the configuration provides a ripe target for buffer overflows, which might attempt to set the value of the useGas cell to false in order to obtain free computation. We are not planning on ever using it with a value of false, so we delete it.
Previously we were parsing the json tests in python, then converting them to KORE and passing them to the backend which then used the kore parser to parse them. This is fairly inefficient, because we end up parsing things twice. The solution is pretty straightforward. We simply send the entire json file to the backend as a single `String`, then invoke the llvm backend's json parser, which is extremely fast, on the resulting term. It's a fairly basic change, but it significantly improves performance. Time on the base branch: ``` real 6m21.214s user 75m41.967s sys 3m35.565s ``` Time on the branch containing the change: ``` real 5m23.010s user 46m6.622s sys 2m47.065s ```
We measured which opcodes are most expensive. As a result of these measurements, we have identified 8 opcodes we want to try to add to optimizations.md. Four of them are included in this PR: ISZERO, JUMPDEST, JUMP, and JUMPI.
I am attempting to change how I maintain the history of our forks so that it will be easy to present clean, up-to-date diffs at any moment to the RV team, and also keep history clean and free from messy merges. As a result, I need a staging branch to exist that I can use to push code that I need to run CI on that will not become part of a pull request but will instead be force pushed to master when I rebase our diffs on top of the latest upstream master. This PR changes the triggers of the workflow slightly so it also triggers on pushes to the specifically named branch.
This is a first draft for the low-level API that will be used to communicate with the DSL. Note that many of the data types used in this draft are simply 64-bit integers. These are placeholders and I welcome your input as to what would be a recommended data type for each such placeholder.
This PR adds the Kompile and Krun flags to the KEVM interface to be built with proof hints instrumentation and to execute a KEVM program to output the expected Proof Hints. Following the same steps present in KEVM's [README](https://github.com/Pi-Squared-Inc/evm-semantics?tab=readme-ov-file#k-definitions), we can build it with: ```bash poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.llvm --arg llvm-proof-hint-instrumentation=true ``` A KEVM program in a JSON format can be executed as: ```bash poetry -C kevm-pyk run kevm-pyk run -v --proof-hint tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --target llvm --mode NORMAL --schedule SHANGHAI --chainid 1 ``` Unfortunately, we won't have support in Pyk right away. Therefore, we implemented a workaround to save the parsed file into `add11.kore`, following the example above. To output the hints, you'll need to execute the `krun` command yourself following the example below: ```bash krun add11.kore --definition /home/robertorosmaninho/.cache/kdist-61cab2d/evm-semantics/llvm --output kore --parser cat --term --proof-output > add11.hints ``` Then, following the known approach, we have the human-readable Hints file: ```bash kore-rich-header /home/robertorosmaninho/.cache/kdist-61cab2d/evm-semantics/llvm/definition.kore -o add11.header kore-proof-trace add11.header add11.hints --verbose > add11.hints.txt ```
…binary or poetry. (#14) Previously, we couldn't parse the `--proof-hints` flag to `krun` through the poetry/`kevm` binary. As pyk now has support for calling `krun` with this flag and returning `bytes` as expected, we can now call this new function `run_proof_hint` and write the bytes to the stdout buffer.
Robertorosmaninho
changed the title
#loadProgram to avoid computing #computeValidJumpDests(PGM)
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.
No description provided.