Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make kevm-dist extensible #2114

Merged
merged 8 commits into from
Oct 18, 2023
Merged

Make kevm-dist extensible #2114

merged 8 commits into from
Oct 18, 2023

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Oct 13, 2023 •
edited
Loading

Preparatory refactoring for runtimeverification/kontrol#61.

  • Define class Target and implement all build tasks in terms of it
  • Load targets from plugins registered under group kdist
  • Add command kevm-dist list to list registered targets

This makes moving the foundry target to the kontrol repo as easy as defining and exposing __TARGETS__ there.

What's still missing (this can potentially be turned into kbuild 1.0):

@tothtamas28 tothtamas28 self-assigned this Oct 13, 2023
@tothtamas28 tothtamas28 force-pushed the refactor-kevm-dist branch 2 times, most recently from a7f9fbe to afc7eef Compare October 16, 2023 16:24
@tothtamas28 tothtamas28 marked this pull request as ready for review October 17, 2023 14:56
@tothtamas28 tothtamas28 requested a review from ehildenb October 17, 2023 14:56
@rv-jenkins rv-jenkins merged commit 5524987 into master Oct 18, 2023
@rv-jenkins rv-jenkins deleted the refactor-kevm-dist branch October 18, 2023 17:02
geo2a pushed a commit that referenced this pull request Oct 27, 2023
@tothtamas28 @geo2a
Make kevm-dist extensible (#2114)
d50135d 
* Extract class `Target` and `KEVMTarget`

* Use `Target` for building

* Separate CLI, framework and targets

* Load targets from plugins

* Fix error message

* Rename plugin group

* Write directly to `output_dir`

* Set Version: 1.0.317

---------

Co-authored-by: devops <devops@runtimeverification.com>
rv-jenkins added a commit that referenced this pull request Nov 9, 2023
@geo2a @rv-jenkins
@ehildenb @qian-hu @PetarMax @palinatolmach @nwatson22 @tothtamas28 @F-WRunTime @anvacaru @Scott-Guest @jberthold
Add '--smt-tactic <s-expression>' command-line option (#2086)
1f9f6dd 
* Add '--smt-tactic <s-expression>' command-line option

* Set Version: 1.0.305

* Set Version: 1.0.307

* Set Version: 1.0.308

* Small build updates for LLVM backend, timing updates (#2098)

* kevm-pyk/{kompile,__main__}: do not turn on debug symbols by default

* kevm-pyk/dist: parallelize plugin build

* kevm-pyk/__main__: add proof timing information to info log

* Set Version: 1.0.308

* kevm-pyk/dist: typo

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Update dependency: kevm-pyk/src/kevm_pyk/kproj/plugin (#2100)

* kevm-pyk/src/kevm_pyk/kproj/plugin: Set Version c095983f3aec21c52f00b2d433202052ad7db104

* Set Version: 1.0.309

* kevm-pyk/: sync poetry files pyk version v0.1.448

* deps/blockchain-k-plugin_release: sync release file version c095983f3aec21c52f00b2d433202052ad7db104

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Upstream lemmas from Wormhole engagement (#1866)

* Add notMaxUInt constants

* Add bitwise-arithmetic lemmas

* Upstream bytes-simplification lemmas from Wormhole

* Upstream lemmas from Wormhole engagement

* Set Version: 1.0.187

* Revert "Upstream lemmas from Wormhole engagement"

This reverts commit 22f8392.

* Set Version: 1.0.210

* Update include/kframework/word.md

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

* Set Version: 1.0.211

* Set Version: 1.0.212

* Set Version: 1.0.213

* Set Version: 1.0.219

* Set Version: 1.0.227

* Set Version: 1.0.228

* generalize lemmas

* Set Version: 1.0.244

* Set Version: 1.0.249

* Set Version: 1.0.296

* Set Version: 1.0.309

* cleanup

* simplification fix

* Set Version: 1.0.310

* removing simplification

* Fix simplification

* Add claims for lemmas

* Update bytes-simplification.k

* Add more claims for lemmas

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>

* Add `setGas` cheatcode (#2101)

* Add `setGas` cheatcode

* Set Version: 1.0.310

* Set Version: 1.0.311

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

* .github/workflows: use z3-images repository for prebuilt z3 images (#2104)

* .github/workflows: use z3-images repository for prebuilt z3 images

* Set Version: 1.0.312

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Support for init bytecode (#2096)

* Split off support for init bytecode for kevm

* Set Version: 1.0.308

* Set Version: 1.0.308

* Fix formatting

* Set Version: 1.0.309

* Set Version: 1.0.310

* Set Version: 1.0.312

* Fix formatting

* Set Version: 1.0.313

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Run prover tests on fast CI machines (#2108)

* .github/test-pr: run fonudry tests on fast CI runners

* Set Version: 1.0.312

* .github/test-pr: also run normal KClaim style proofs on fast CI runners

* Set Version: 1.0.313

* Set Version: 1.0.314

* .github/test-pr: reduce parallelism on test-suite

* .github/test-pr: correct way to adjust parallelism

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

* Update dependency: deps/pyk_release (#2092)

* deps/pyk_release: Set Version v0.1.449

* Set Version: 1.0.307

* kevm-pyk/: sync poetry files pyk version v0.1.449

* deps/k_release: sync release file version 6.0.118

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.450

* Set Version: 1.0.308

* kevm-pyk/: sync poetry files pyk version v0.1.450

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.451

* kevm-pyk/: sync poetry files pyk version v0.1.451

* deps/k_release: sync release file version 6.0.119

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.452

* kevm-pyk/: sync poetry files pyk version v0.1.452

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.453

* kevm-pyk/: sync poetry files pyk version v0.1.453

* deps/k_release: sync release file version 6.0.120

* flake.{nix,lock}: update Nix derivations

* kevm-pyk/src/kevm_pyk/kproj/plugin: Set Version 1aa2e24669529ea14d806d5b7f9116c65780f368

* deps/blockchain-k-plugin_release: sync release file version 1aa2e24669529ea14d806d5b7f9116c65780f368

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.454

* kevm-pyk/: sync poetry files pyk version v0.1.454

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.455

* kevm-pyk/: sync poetry files pyk version v0.1.455

* deps/k_release: sync release file version 6.0.121

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.456

* kevm-pyk/: sync poetry files pyk version v0.1.456

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.457

* kevm-pyk/: sync poetry files pyk version v0.1.457

* flake.{nix,lock}: update Nix derivations

* Set Version: 1.0.309

* deps/pyk_release: Set Version v0.1.458

* kevm-pyk/: sync poetry files pyk version v0.1.458

* deps/k_release: sync release file version 6.0.124

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.459

* kevm-pyk/: sync poetry files pyk version v0.1.459

* flake.{nix,lock}: update Nix derivations

* deps/blockchain-k-plugin_release: update to newest version

* Set Version: 1.0.312

* kevm-pyk/: sync poetry files pyk version v0.1.459

* deps/blockchain-k-plugin_release: sync release file version c095983f3aec21c52f00b2d433202052ad7db104

* flake.{nix,lock}: update Nix derivations

* bluckchain-k-plugin: update version

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.460

* kevm-pyk/: sync poetry files pyk version v0.1.460

* deps/k_release: sync release file version 6.0.128

* flake.{nix,lock}: update Nix derivations

* kevm-pyk/word: make sure #rangeUInt(5, ...) is defined

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.461

* kevm-pyk/: sync poetry files pyk version v0.1.461

* deps/k_release: sync release file version 6.0.133

* flake.{nix,lock}: update Nix derivations

* Set Version: 1.0.313

* kevm-pyk/: sync poetry files pyk version v0.1.461

* Set Version: 1.0.314

* Set Version: 1.0.315

* kevm-pyk/: sync poetry files pyk version v0.1.461

* Update expected output

* kevm-pyk/: sync poetry files pyk version v0.1.461

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>

* Update Dockerfile (#2110)

* Update Dockerfile

Updating repository for image pull for z3

* Set Version: 1.0.316

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Make `kevm-dist` extensible (#2114)

* Extract class `Target` and `KEVMTarget`

* Use `Target` for building

* Separate CLI, framework and targets

* Load targets from plugins

* Fix error message

* Rename plugin group

* Write directly to `output_dir`

* Set Version: 1.0.317

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Extend prank rules for create (#2119)

* extend prank rules for create

* Set Version: 1.0.318

* Apply suggestions from code review

Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

* Remove `HASKELL_STANDALONE` and `FOUNDRY` from `KompileTarget` (#2121)

* Remove `HASKELL_STANDALONE` and `FOUNDRY` from `KompileTarget`

* Set Version: 1.0.318

* Set Version: 1.0.319

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Implement dependency handling for `kdist` (#2126)

* Rename function `build` to `_build_target`

* Extract function `build`

* Remove parameter `command`

* Add default values for parameters

* Extract statement

* Remove parameter `debug`

* Refactor `build`

* Remove unused private variable

* Replace import

* Make `DIST_DIR` private

* Slide statements

* Rename distribution directory

* Add method `deps` to `Target`

* Add optional parameter `deps` to `KEVMTarget.__init__`

* Add `plugin` dependency to `llvm`

* Do not expose loaded targets

* Eliminate hard-coded dependency structure

* Extract module `api`

* Change parameter type

* Add parameter `deps` to `build`

* Inject dependency paths into build tasks

* Set Version: 1.0.320

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Allow selecting fail_fast parameter for advance_proof (#2117)

* Allow selecting fail_fast parameter for advance_proof

* Set Version: 1.0.317

* Set Version: 1.0.318

* Set Version: 1.0.319

* Update kevm-pyk/src/kevm_pyk/cli.py

Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

* Set Version: 1.0.320

* Set Version: 1.0.321

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

* Disable testing of Foundry functionality (#2127)

* .github/, package/version: remove tests of foundry functionality

* Set Version: 1.0.320

* .github/test-pr: remove profile test which only ran kontrol tests

* Revert ".github/test-pr: remove profile test which only ran kontrol tests"

This reverts commit 4df1571.

* kevm-pyk/src/tests/profiling/test_foundry_prove: remove test of kontrox functionality

* Set Version: 1.0.322

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Use `Bytes` to represent byte strings instead of `String` (#2128)

* Updated all calls to blockchain plugin to pass Bytes rather than String

* Change rlpEncode/rlpDecode to use Bytes rather than String

* Restore unintentionally deleted call to #unparseByteStack in #rplDecodeTransaction

* Update verification.k for new Keccak256 interface

* Add wrapper arounds new plugin interface. More pervasively use Bytes over Strings.

* Set Version: 1.0.323

* Set Version: 1.0.323

* Formatting and small clean up.

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Simplify job `kevm-pyk-profile` (#2132)

* Simplify job `kevm-pyk-profile`

This job no longer requires K, moved to public runner.

* Set Version: 1.0.324

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Update dependency: deps/pyk_release (#2111)

* deps/pyk_release: Set Version v0.1.463

* Set Version: 1.0.316

* kevm-pyk/: sync poetry files pyk version v0.1.463

* deps/k_release: sync release file version 6.0.138

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.464

* Set Version: 1.0.317

* kevm-pyk/: sync poetry files pyk version v0.1.464

* deps/k_release: sync release file version 6.0.139

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.465

* kevm-pyk/: sync poetry files pyk version v0.1.465

* deps/k_release: sync release file version 6.0.144

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.466

* kevm-pyk/: sync poetry files pyk version v0.1.466

* deps/k_release: sync release file version 6.0.145

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.467

* kevm-pyk/: sync poetry files pyk version v0.1.467

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.468

* kevm-pyk/: sync poetry files pyk version v0.1.468

* deps/k_release: sync release file version 6.0.146

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.469

* kevm-pyk/: sync poetry files pyk version v0.1.469

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.470

* kevm-pyk/: sync poetry files pyk version v0.1.470

* flake.{nix,lock}: update Nix derivations

* Set Version: 1.0.318

* deps/pyk_release: Set Version v0.1.471

* kevm-pyk/: sync poetry files pyk version v0.1.471

* deps/k_release: sync release file version 6.0.148

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.472

* Set Version: 1.0.319

* kevm-pyk/: sync poetry files pyk version v0.1.472

* deps/k_release: sync release file version 6.0.150

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.473

* kevm-pyk/: sync poetry files pyk version v0.1.473

* deps/k_release: sync release file version 6.0.152

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.474

* kevm-pyk/: sync poetry files pyk version v0.1.474

* deps/k_release: sync release file version 6.0.153

* flake.{nix,lock}: update Nix derivations

* Set Version: 1.0.320

* update poetry.lock

* add inotify dependency

* add fixture to run kserver

* kevm-pyk/: sync poetry files pyk version v0.1.474

* create dir if it doesn't exist

* deps/pyk_release: Set Version v0.1.475

* Set Version: 1.0.321

* kevm-pyk/: sync poetry files pyk version v0.1.475

* deps/k_release: sync release file version 6.0.156

* flake.{nix,lock}: update Nix derivations

* Set Version: 1.0.323

* EXPERIMENT: reduce test parallelism to 4

* EXPERIMENT: remove normal label for runners

* Revert "EXPERIMENT: reduce test parallelism to 4"

This reverts commit e8a5a6f.

* EXPERIMENT: reduce test parallelism to 4

* Set Version: 1.0.324

* kevm-pyk/: sync poetry files pyk version v0.1.475

* use newer pyk version

* kevm-pyk/: sync poetry files pyk version v0.1.477

* deps/k_release: sync release file version 6.0.161

* flake.{nix,lock}: update Nix derivations

* limit max_depth to 300 in pyk_prove tests (workaround)

* run proof tests with different parallelism degree

* deps/pyk_release: Set Version v0.1.478

* kevm-pyk/: sync poetry files pyk version v0.1.478

* deps/k_release: sync release file version 6.0.163

* flake.{nix,lock}: update Nix derivations

* Revert "run proof tests with different parallelism degree"

This reverts commit c8d2eaa.

* Set Version: 1.0.325

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Dwight Guth <dwight.guth@runtimeverification.com>
Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

* Use Proof names and IDs in bug report archives (#2125)

* provide an ID when creating KoreClient

* Set Version: 1.0.326

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Better directory management for `kdist` (#2134)

* Lock target directories for `kevm-dist build`

* Switch to `ProcessPoolExecutor`

* Run build in temporary directory

* Set Version: 1.0.327

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Remove testing infrastructure related to kontrolx (#2135)

* .gitignore, tests/specs/examples: commit bin-runtime files

* kevm-pyk/test_prove: simplify compilation process now that we dont need to generate K code

* .gitmodules: remove forge-std

* kevm-pyk/: remove more references to foundry tests

* kevm-pyk/src/tests/integration/test-data: remove references to foundry tests

* kevm-pyk/src/tests/integration/test_{foundry_prove,solc_to_k}: remove unused files

* Set Version: 1.0.326

* tests/foundry/lib/forge-std: remove submodule

* Set Version: 1.0.328

---------

Co-authored-by: devops <devops@runtimeverification.com>

* Set Version: 1.0.329

* Set Version: 1.0.343

* Set Version: 1.0.344

* Set Version: 1.0.345

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Co-authored-by: qian-hu <88806138+qian-hu@users.noreply.github.com>
Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>
Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com>
Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>
Co-authored-by: Scott Guest <scott.guest@runtimeverification.com>
Co-authored-by: Dwight Guth <dwight.guth@runtimeverification.com>
Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
Co-authored-by: Andrei <andrei.vacaru@runtimeverification.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ehildenb ehildenb ehildenb approved these changes

Assignees

@tothtamas28 tothtamas28

Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tothtamas28 @ehildenb @rv-jenkins