Add '--smt-tactic <s-expression>' command-line option (#2086)

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>

* Add `setGas` cheatcode (#2101)

* Add `setGas` cheatcode

* Set Version: 1.0.310

* Set Version: 1.0.311

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

* .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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

* 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 <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

* Update Dockerfile (#2110)

* Update Dockerfile

Updating repository for image pull for z3

* Set Version: 1.0.316

---------

Co-authored-by: devops <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* Set Version: 1.0.320

* Set Version: 1.0.321

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>
Co-authored-by: Dwight Guth <[email protected]>
Co-authored-by: Jost Berthold <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* Set Version: 1.0.329

* Set Version: 1.0.343

* Set Version: 1.0.344

* Set Version: 1.0.345

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: qian-hu <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>
Co-authored-by: Noah Watson <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Co-authored-by: Freeman <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Scott Guest <[email protected]>
Co-authored-by: Dwight Guth <[email protected]>
Co-authored-by: Jost Berthold <[email protected]>
Co-authored-by: Andrei <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.344"
+version = "1.0.345"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.344'
+VERSION: Final = '1.0.345'

kevm-pyk/src/kevm_pyk/utils.py

@@ -304,6 +304,7 @@ def legacy_explore(
     llvm_definition_dir: Path | None = None,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,
+    smt_tactic: str | None = None,
     bug_report: BugReport | None = None,
     haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
     haskell_log_entries: Iterable[str] = (),
@@ -323,6 +324,7 @@ def legacy_explore(
             bug_report=bug_report,
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
+            smt_tactic=smt_tactic,
             haskell_log_format=haskell_log_format,
             haskell_log_entries=haskell_log_entries,
             log_axioms_file=log_axioms_file,

package/version

@@ -1 +1 @@
-1.0.344
+1.0.345