runtimeverification / blockchain-k-plugin Goto Github PK

When calling make in KEVM now, I get an error with formatting in this repo:

poetry install
Installing dependencies from lock file
Warning: poetry.lock is not consistent with pyproject.toml. You may be getting improper dependencies. Run `poetry lock [--no-update]` to fix it.

No dependencies to install or update

Installing the current project: kevm-pyk (1.0.529)
poetry run flake8 src
poetry run mypy src
Success: no issues found in 29 source files
poetry run autoflake --quiet --check src
poetry run isort --check src
ERROR: /home/dev/src/evm-semantics/kevm-pyk/src/kevm_pyk/kproj/plugin/tests/test.py Imports are incorrectly sorted and/or formatted.
make: *** [Makefile:89: check-isort] Error 1

I guess that we need to:

• Enable codestyle checks on CI here for the python code.

Is there a license for this repo?

Currently, the interface presumes that Strings can be treated as raw byte arrays. This will no longer be true once we support Unicode, so the hooks should be updated to use Bytes instead.

Discussions with @goodlyrottenapple and @jberthold led us to conclude we may want to build a combined library (statically?) that includes all the dependencies like cryptopp etc.

As the number of projects depending on the plugin increases, it would be helpful to have a checklist of current plugin users so that we are sure that no project falls through the cracks when we update.

There are several changes that need to be made to facilitate (i) modularity of the KEVM build, and (ii) hooks needed by the Michelson Semantics.

Here is the proposed upgrade path:

1. add some new hash functions that Michelson needs

• add a libcrypto++ submodule so that we can still do test builds in this repo --- because the libcrypto++ package in Ubuntu/Debian doesn't include the needed symbols
• add the hash functions blake2 and sha2-512

2. upstream the KEVM hooks/build recipes

• add all KEVM hooks to the plugin
• hide the Michelson hooks that depend on a more recent version of libcrypto++ behind a tangle tag
• make KEVM source the plugin hook file and delete its internal copy of the hook file
• upstream the KEVM build recipes for its crypto submodules and directly call the plugin Makefile build recipes

3. split out the hooks in build plugin file into separate modules based on which library they use

• update the plugin hook files and build test (also update plugin hook names, refer to runtimeverification/k#1216)
• update KEVM so that it sources the new files correctly

log vmquery and Code/Blockhash/Account/StorageData messages.

See all bug reports here: https://bugs.launchpad.net/ubuntu/+source/libcrypto++/

In particular, the bug that affects us is: https://bugs.launchpad.net/ubuntu/+source/libcrypto++/+bug/1876166

This seems like a similar bug: https://bugs.launchpad.net/ubuntu/+source/libcrypto++/+bug/660171

This affects us because we want to use some of the missing symbols as crypto hooks. This forces us to have a more complex build/package process for any semantics that uses those hooks.