diff --git a/Dockerfile b/Dockerfile
index 6c0b3e624d..c3341a83e0 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -11,7 +11,6 @@ RUN apt-get update \
flex \
gcc \
jq \
- libboost-all-dev \
libboost-test-dev \
libcrypto++-dev \
libffi-dev \
@@ -19,7 +18,6 @@ RUN apt-get update \
libjemalloc-dev \
libmpfr-dev \
libprocps-dev \
- libprotobuf-dev \
libsecp256k1-dev \
libssl-dev \
libtool \
@@ -32,7 +30,6 @@ RUN apt-get update \
openjdk-11-jdk \
pandoc \
pkg-config \
- protobuf-compiler \
python3 \
python-pygments \
python-recommonmark \
diff --git a/Jenkinsfile b/Jenkinsfile
index a96a5ee131..5e37633015 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -8,26 +8,14 @@ pipeline {
PACKAGE = 'kevm'
ROOT_URL = 'https://github.com/kframework/evm-semantics/releases/download'
}
- options {
- ansiColor('xterm')
- }
+ options { ansiColor('xterm') }
stages {
stage("Init title") {
- when {
- changeRequest()
- beforeAgent true
- }
- steps {
- script {
- currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}"
- }
- }
+ when { changeRequest() }
+ steps { script { currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}" } }
}
stage('Build and Test') {
- when {
- changeRequest()
- beforeAgent true
- }
+ when { changeRequest() }
agent {
dockerfile {
additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
@@ -36,56 +24,15 @@ pipeline {
}
}
stages {
- stage('Dependencies') {
- parallel {
- stage('K') {
- steps {
- sh '''
- make deps RELEASE=true
- '''
- }
- }
- stage('Tests') {
- steps {
- sh '''
- make split-tests -j3
- '''
- }
- }
- }
- }
- stage('Build') {
- steps {
- sh '''
- make build -j4
- '''
- }
- }
+ stage('K Dependencies') { steps { sh 'make deps RELEASE=true' } }
+ stage('Build') { steps { sh 'make build RELEASE=true -j6' } }
stage('Test Execution') {
failFast true
options { timeout(time: 20, unit: 'MINUTES') }
parallel {
- stage('Conformance (LLVM)') {
- steps {
- sh '''
- make test-conformance -j8 TEST_CONCRETE_BACKEND=llvm
- '''
- }
- }
- stage('VM (Haskell)') {
- steps {
- sh '''
- make test-vm -j8 TEST_CONCRETE_BACKEND=haskell
- '''
- }
- }
- stage('Conformance (Web3)') {
- steps {
- sh '''
- make test-web3 -j8
- '''
- }
- }
+ stage('Conformance (LLVM)') { steps { sh 'make test-conformance -j8 TEST_CONCRETE_BACKEND=llvm' } }
+ stage('VM (Haskell)') { steps { sh 'make test-vm -j8 TEST_CONCRETE_BACKEND=haskell' } }
+ stage('Conformance (Web3)') { steps { sh 'make test-web3 -j8' } }
}
}
stage('Proofs') {
@@ -94,79 +41,70 @@ pipeline {
timeout(time: 55, unit: 'MINUTES')
}
parallel {
- stage('Java + Haskell') {
- steps {
- sh '''
- make test-prove -j6
- '''
- }
- }
- stage('Haskell (dry-run)') {
- steps {
- sh '''
- make test-prove -j2 KPROVE_OPTIONS='--dry-run' TEST_SYMBOLIC_BACKEND='haskell'
- '''
- }
- }
+ stage('Java + Haskell') { steps { sh 'make test-prove -j6' } }
+ stage('Haskell (dry-run)') { steps { sh 'make test-prove -j2 KPROVE_OPTIONS=--dry-run TEST_SYMBOLIC_BACKEND=haskell' } }
}
}
stage('Test Interactive') {
failFast true
options { timeout(time: 35, unit: 'MINUTES') }
parallel {
- stage('LLVM krun') {
- steps {
- sh '''
- make test-interactive-run TEST_CONCRETE_BACKEND=llvm
- '''
- }
- }
- stage('Java krun') {
- steps {
- sh '''
- make test-interactive-run TEST_CONCRETE_BACKEND=java
- '''
- }
- }
- stage('Haskell krun') {
- steps {
- sh '''
- make test-interactive-run TEST_CONCRETE_BACKEND=haskell
- '''
- }
- }
- stage('LLVM Kast') {
- steps {
- sh '''
- make test-parse TEST_CONCRETE_BACKEND=llvm
- '''
- }
- }
- stage('Failing tests') {
- steps {
- sh '''
- make test-failure TEST_CONCRETE_BACKEND=llvm
- '''
- }
- }
- stage('Java KLab') {
- steps {
- sh '''
- make test-klab-prove TEST_SYMBOLIC_BACKEND=java
- '''
- }
- }
- stage('Haskell Search') {
- steps {
- sh '''
- make test-interactive-search TEST_SYMBOLIC_BACKEND=haskell -j4
- '''
- }
- }
- stage('KEVM help') {
- steps {
+ stage('LLVM krun') { steps { sh 'make test-interactive-run TEST_CONCRETE_BACKEND=llvm' } }
+ stage('Java krun') { steps { sh 'make test-interactive-run TEST_CONCRETE_BACKEND=java' } }
+ stage('Haskell krun') { steps { sh 'make test-interactive-run TEST_CONCRETE_BACKEND=haskell' } }
+ stage('LLVM Kast') { steps { sh 'make test-parse TEST_CONCRETE_BACKEND=llvm' } }
+ stage('Failing tests') { steps { sh 'make test-failure TEST_CONCRETE_BACKEND=llvm' } }
+ stage('Java KLab') { steps { sh 'make test-klab-prove TEST_SYMBOLIC_BACKEND=java' } }
+ stage('Haskell Search') { steps { sh 'make test-interactive-search TEST_SYMBOLIC_BACKEND=haskell -j4' } }
+ stage('KEVM help') { steps { sh './kevm help' } }
+ }
+ }
+ }
+ }
+ stage('Deploy') {
+ when { branch 'master' }
+ agent { dockerfile { reuseNode true } }
+ stages {
+ stage('Update Dependents') {
+ steps {
+ build job: 'rv-devops/master', propagate: false, wait: false \
+ , parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
+ , string(name: 'PR_REVIEWER', value: 'ehildenb') \
+ , string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/firefly') \
+ , string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
+ ]
+ build job: 'rv-devops/master', propagate: false, wait: false \
+ , parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
+ , string(name: 'PR_REVIEWER', value: 'ehildenb') \
+ , string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/erc20-verification') \
+ , string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
+ ]
+ }
+ }
+ stage('Jello Paper') {
+ steps {
+ sshagent(['2b3d8d6b-0855-4b59-864a-6b3ddf9c9d1a']) {
+ dir("kevm-${env.VERSION}-jello-paper") {
sh '''
- ./kevm help
+ git config --global user.email "admin@runtimeverification.com"
+ git config --global user.name "RV Jenkins"
+ mkdir -p ~/.ssh
+ echo 'host github.com' > ~/.ssh/config
+ echo ' hostname github.com' >> ~/.ssh/config
+ echo ' user git' >> ~/.ssh/config
+ echo ' identityagent SSH_AUTH_SOCK' >> ~/.ssh/config
+ echo ' stricthostkeychecking accept-new' >> ~/.ssh/config
+ chmod go-rwx -R ~/.ssh
+ ssh github.com || true
+ git clone 'ssh://github.com/kframework/evm-semantics.git'
+ cd evm-semantics
+ git checkout -B gh-pages origin/master
+ rm -rf .build .gitignore .gitmodules cmake deps Dockerfile Jenkinsfile kast-json.py kevm kore-json.py LICENSE Makefile media package
+ git add ./
+ git commit -m 'gh-pages: remove unrelated content'
+ git fetch origin gh-pages
+ git merge --strategy ours FETCH_HEAD
+ git push origin gh-pages
'''
}
}
@@ -174,22 +112,5 @@ pipeline {
}
}
}
- stage('Update Dependents') {
- when { branch 'master' }
- steps {
- build job: 'rv-devops/master', propagate: false, wait: false \
- , parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
- , string(name: 'PR_REVIEWER', value: 'ehildenb') \
- , string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/firefly') \
- , string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
- ]
- build job: 'rv-devops/master', propagate: false, wait: false \
- , parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
- , string(name: 'PR_REVIEWER', value: 'ehildenb') \
- , string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/erc20-verification') \
- , string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
- ]
- }
- }
}
}
diff --git a/Makefile b/Makefile
index c7bdb85887..ffd88c0f29 100644
--- a/Makefile
+++ b/Makefile
@@ -1,38 +1,37 @@
# Settings
# --------
+DEPS_DIR := deps
BUILD_DIR := .build
SUBDEFN_DIR := .
DEFN_BASE_DIR := $(BUILD_DIR)/defn
DEFN_DIR := $(DEFN_BASE_DIR)/$(SUBDEFN_DIR)
BUILD_LOCAL := $(abspath $(BUILD_DIR)/local)
+LOCAL_LIB := $(BUILD_LOCAL)/lib
-LIBRARY_PATH := $(BUILD_LOCAL)/lib
+K_SUBMODULE := $(DEPS_DIR)/k
+ifneq (,$(wildcard $(K_SUBMODULE)/k-distribution/target/release/k/bin/*))
+ K_RELEASE ?= $(abspath $(K_SUBMODULE)/k-distribution/target/release/k)
+else
+ K_RELEASE ?= $(dir $(shell which kompile))..
+endif
+K_BIN := $(K_RELEASE)/bin
+K_LIB := $(K_RELEASE)/lib/kframework
+export K_RELEASE
+
+LIBRARY_PATH := $(LOCAL_LIB)
C_INCLUDE_PATH += :$(BUILD_LOCAL)/include
CPLUS_INCLUDE_PATH += :$(BUILD_LOCAL)/include
-PKG_CONFIG_PATH := $(LIBRARY_PATH)/pkgconfig
+PATH := $(K_BIN):$(PATH)
export LIBRARY_PATH
export C_INCLUDE_PATH
export CPLUS_INCLUDE_PATH
-export PKG_CONFIG_PATH
-
-INSTALL_PREFIX := /usr/local
-INSTALL_DIR ?= $(DESTDIR)$(INSTALL_PREFIX)/bin
+export PATH
-DEPS_DIR := deps
-K_SUBMODULE := $(abspath $(DEPS_DIR)/k)
PLUGIN_SUBMODULE := $(abspath $(DEPS_DIR)/plugin)
export PLUGIN_SUBMODULE
-K_RELEASE ?= $(K_SUBMODULE)/k-distribution/target/release/k
-K_BIN := $(K_RELEASE)/bin
-K_LIB := $(K_RELEASE)/lib
-export K_RELEASE
-
-PATH := $(K_BIN):$(PATH)
-export PATH
-
# need relative path for `pandoc` on MacOS
PANDOC_TANGLE_SUBMODULE := $(DEPS_DIR)/pandoc-tangle
TANGLER := $(PANDOC_TANGLE_SUBMODULE)/tangle.lua
@@ -42,21 +41,20 @@ export LUA_PATH
.PHONY: all clean distclean \
deps all-deps llvm-deps haskell-deps repo-deps k-deps plugin-deps libsecp256k1 libff \
- build build-java build-node build-haskell build-llvm build-web3 \
- defn java-defn node-defn web3-defn haskell-defn llvm-defn \
- split-tests \
+ build build-java build-specs build-haskell build-llvm build-web3 \
+ defn java-defn specs-defn web3-defn haskell-defn llvm-defn \
test test-all test-conformance test-rest-conformance test-all-conformance test-slow-conformance test-failing-conformance \
test-vm test-rest-vm test-all-vm test-bchain test-rest-bchain test-all-bchain \
test-web3 test-all-web3 test-failing-web3 \
test-prove test-failing-prove \
test-prove-benchmarks test-prove-functional test-prove-opcodes test-prove-erc20 test-prove-bihu test-prove-examples \
- test-klab-prove \
+ test-prove-imp-specs test-klab-prove \
test-parse test-failure \
test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search \
media media-pdf metropolis-theme
.SECONDARY:
-all: build split-tests
+all: build
clean:
rm -rf $(DEFN_BASE_DIR)
@@ -68,131 +66,108 @@ distclean:
# Non-K Dependencies
# ------------------
-libsecp256k1_out := $(LIBRARY_PATH)/pkgconfig/libsecp256k1.pc
-libff_out := $(LIBRARY_PATH)/libff.a
+libsecp256k1_out := $(LOCAL_LIB)/pkgconfig/libsecp256k1.pc
+libff_out := $(LOCAL_LIB)/libff.a
libsecp256k1: $(libsecp256k1_out)
libff: $(libff_out)
-$(DEPS_DIR)/secp256k1/autogen.sh:
- git submodule update --init --recursive -- $(DEPS_DIR)/secp256k1
-
$(libsecp256k1_out): $(DEPS_DIR)/secp256k1/autogen.sh
- cd $(DEPS_DIR)/secp256k1/ \
- && ./autogen.sh \
+ cd $(DEPS_DIR)/secp256k1/ \
+ && ./autogen.sh \
&& ./configure --enable-module-recovery --prefix="$(BUILD_LOCAL)" \
- && $(MAKE) \
+ && $(MAKE) \
&& $(MAKE) install
UNAME_S := $(shell uname -s)
ifeq ($(UNAME_S),Linux)
- LIBFF_CMAKE_FLAGS=
- LINK_PROCPS=-lprocps
+ LIBFF_CMAKE_FLAGS=
else
- LIBFF_CMAKE_FLAGS=-DWITH_PROCPS=OFF
- LINK_PROCPS=
+ LIBFF_CMAKE_FLAGS=-DWITH_PROCPS=OFF
endif
-LIBFF_CC := clang-8
-LIBFF_CXX := clang++-8
-
-$(DEPS_DIR)/libff/CMakeLists.txt:
- git submodule update --init --recursive -- $(DEPS_DIR)/libff
-
$(libff_out): $(DEPS_DIR)/libff/CMakeLists.txt
@mkdir -p $(DEPS_DIR)/libff/build
- cd $(DEPS_DIR)/libff/build \
- && CC=$(LIBFF_CC) CXX=$(LIBFF_CXX) cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$(BUILD_LOCAL) $(LIBFF_CMAKE_FLAGS) \
- && make -s -j4 \
+ cd $(DEPS_DIR)/libff/build \
+ && cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$(BUILD_LOCAL) $(LIBFF_CMAKE_FLAGS) \
+ && make -s -j4 \
&& make install
# K Dependencies
# --------------
+K_JAR := $(K_SUBMODULE)/k-distribution/target/release/k/lib/java/kernel-1.0-SNAPSHOT.jar
+
deps: repo-deps
repo-deps: tangle-deps k-deps plugin-deps
-k-deps: $(K_SUBMODULE)/make.timestamp
+k-deps: $(K_JAR)
tangle-deps: $(TANGLER)
-plugin-deps: $(PLUGIN_SUBMODULE)/make.timestamp
+plugin-deps: $(PLUGIN_SUBMODULE)/client-c/main.cpp
BACKEND_SKIP=-Dhaskell.backend.skip -Dllvm.backend.skip
-
ifneq ($(RELEASE),)
-K_BUILD_TYPE := FastBuild
-SEMANTICS_BUILD_TYPE := Release
-KOMPILE_OPTS += -O3
+ K_BUILD_TYPE := FastBuild
+ SEMANTICS_BUILD_TYPE := Release
+ KOMPILE_OPTS += -O3
else
-K_BUILD_TYPE := FastBuild
-SEMANTICS_BUILD_TYPE := Debug
+ K_BUILD_TYPE := FastBuild
+ SEMANTICS_BUILD_TYPE := Debug
endif
-$(K_SUBMODULE)/make.timestamp:
- git submodule update --init --recursive -- $(K_SUBMODULE)
- cd $(K_SUBMODULE) && mvn package -DskipTests -U -Dproject.build.type=${K_BUILD_TYPE} $(BACKEND_SKIP)
- touch $(K_SUBMODULE)/make.timestamp
-
-$(TANGLER):
- git submodule update --init -- $(PANDOC_TANGLE_SUBMODULE)
-
-$(PLUGIN_SUBMODULE)/make.timestamp:
- git submodule update --init --recursive -- $(PLUGIN_SUBMODULE)
- touch $(PLUGIN_SUBMODULE)/make.timestamp
+$(K_JAR):
+ cd $(K_SUBMODULE) && mvn package -DskipTests -U -Dproject.build.type=$(K_BUILD_TYPE) $(BACKEND_SKIP)
# Building
# --------
-build-node: MAIN_DEFN_FILE = evm-node
-build-node: MAIN_MODULE = EVM-NODE
-build-node: SYNTAX_MODULE = EVM-NODE
-build-web3: MAIN_DEFN_FILE = web3
-build-web3: MAIN_MODULE = WEB3
-build-web3: SYNTAX_MODULE = WEB3
MAIN_MODULE := ETHEREUM-SIMULATION
SYNTAX_MODULE := $(MAIN_MODULE)
MAIN_DEFN_FILE := driver
-export MAIN_DEFN_FILE
-k_files := driver.k data.k network.k evm.k evm-types.k json.k krypto.k edsl.k evm-node.k web3.k asm.k state-loader.k serialization.k
+k_files := driver.k data.k network.k evm.k evm-types.k json.k krypto.k edsl.k web3.k asm.k state-loader.k serialization.k evm-imp-specs.k
EXTRA_K_FILES += $(MAIN_DEFN_FILE).k
ALL_K_FILES := $(k_files) $(EXTRA_K_FILES)
llvm_dir := $(DEFN_DIR)/llvm
java_dir := $(DEFN_DIR)/java
+specs_dir := $(DEFN_DIR)/specs
haskell_dir := $(DEFN_DIR)/haskell
-node_dir := $(abspath $(DEFN_DIR)/node)
web3_dir := $(abspath $(DEFN_DIR)/web3)
-export node_dir
export web3_dir
llvm_files := $(patsubst %, $(llvm_dir)/%, $(ALL_K_FILES))
java_files := $(patsubst %, $(java_dir)/%, $(ALL_K_FILES))
+specs_files := $(patsubst %, $(specs_dir)/%, $(ALL_K_FILES))
haskell_files := $(patsubst %, $(haskell_dir)/%, $(ALL_K_FILES))
-node_files := $(patsubst %, $(node_dir)/%, $(ALL_K_FILES))
web3_files := $(patsubst %, $(web3_dir)/%, $(ALL_K_FILES))
-defn_files := $(llvm_files) $(java_files) $(haskell_files) $(node_files) $(web3_files)
+defn_files := $(llvm_files) $(java_files) $(specs_files) $(haskell_files) $(web3_files)
java_kompiled := $(java_dir)/$(MAIN_DEFN_FILE)-kompiled/timestamp
-node_kompiled := $(DEFN_DIR)/vm/kevm-vm
+specs_kompiled := $(specs_dir)/specs-kompiled/timestamp
web3_kompiled := $(web3_dir)/build/kevm-client
haskell_kompiled := $(haskell_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
llvm_kompiled := $(llvm_dir)/$(MAIN_DEFN_FILE)-kompiled/interpreter
-node_kore := $(node_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
+$(web3_kompiled): MAIN_DEFN_FILE := web3
+$(web3_kompiled): MAIN_MODULE := WEB3
+$(web3_kompiled): SYNTAX_MODULE := WEB3
+$(web3_kompiled): web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
+
+export MAIN_DEFN_FILE
# Tangle definition from *.md files
-concrete_tangle := .k:not(.node):not(.symbolic):not(.nobytes):not(.memmap),.standalone,.concrete,.bytes,.membytes
-java_tangle := .k:not(.node):not(.concrete):not(.bytes):not(.memmap):not(.membytes),.standalone,.symbolic,.nobytes
-haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes):not(.memmap),.standalone,.symbolic,.bytes,.membytes
-node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes):not(.memmap),.node,.concrete,.bytes,.membytes
+concrete_tangle := .k:not(.symbolic):not(.nobytes):not(.memmap),.concrete,.bytes,.membytes
+java_tangle := .k:not(.concrete):not(.bytes):not(.memmap):not(.membytes),.symbolic,.nobytes
+haskell_tangle := .k:not(.concrete):not(.nobytes):not(.memmap),.symbolic,.bytes,.membytes
defn: $(defn_files)
llvm-defn: $(llvm_files)
java-defn: $(java_files)
+specs-defn: $(specs_files)
haskell-defn: $(haskell_files)
-node-defn: $(node_files)
web3-defn: $(web3_files)
$(llvm_dir)/%.k: %.md $(TANGLER)
@@ -203,88 +178,87 @@ $(java_dir)/%.k: %.md $(TANGLER)
@mkdir -p $(java_dir)
pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(java_tangle)" $< > $@
+$(specs_dir)/%.k: %.md $(TANGLER)
+ @mkdir -p $(specs_dir)
+ pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(java_tangle)" $< > $@
+
$(haskell_dir)/%.k: %.md $(TANGLER)
@mkdir -p $(haskell_dir)
pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(haskell_tangle)" $< > $@
-$(node_dir)/%.k: %.md $(TANGLER)
- @mkdir -p $(node_dir)
- pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(node_tangle)" $< > $@
-
$(web3_dir)/%.k: %.md $(TANGLER)
@mkdir -p $(web3_dir)
pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(concrete_tangle)" $< > $@
# Kompiling
-build: build-llvm build-haskell build-java build-web3 build-node
+build: build-llvm build-haskell build-java build-specs build-web3
build-java: $(java_kompiled)
-build-node: $(node_kompiled)
+build-specs: $(specs_kompiled)
build-web3: $(web3_kompiled)
build-haskell: $(haskell_kompiled)
build-llvm: $(llvm_kompiled)
-# Java Backend
+# Java
$(java_kompiled): $(java_files)
- $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) --backend java \
- --syntax-module $(SYNTAX_MODULE) $(java_dir)/$(MAIN_DEFN_FILE).k \
- --directory $(java_dir) -I $(java_dir) \
- $(KOMPILE_OPTS)
+ kompile --debug --main-module $(MAIN_MODULE) --backend java \
+ --syntax-module $(SYNTAX_MODULE) $(java_dir)/$(MAIN_DEFN_FILE).k \
+ --directory $(java_dir) -I $(java_dir) \
+ $(KOMPILE_OPTS)
-# Haskell Backend
+# Imperative Specs
-$(haskell_kompiled): $(haskell_files)
- $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) --backend haskell --hook-namespaces KRYPTO \
- --syntax-module $(SYNTAX_MODULE) $(haskell_dir)/$(MAIN_DEFN_FILE).k \
- --directory $(haskell_dir) -I $(haskell_dir) \
- $(KOMPILE_OPTS)
+$(specs_kompiled): MAIN_DEFN_FILE=evm-imp-specs
+$(specs_kompiled): MAIN_MODULE=EVM-IMP-SPECS
+$(specs_kompiled): SYNTAX_MODULE=EVM-IMP-SPECS
-# Node Backend
+$(specs_kompiled): $(specs_files)
+ kompile --debug --main-module $(MAIN_MODULE) --backend java \
+ --syntax-module $(SYNTAX_MODULE) $(specs_dir)/$(MAIN_DEFN_FILE).k \
+ --directory $(specs_dir) -I $(specs_dir) \
+ $(KOMPILE_OPTS)
-$(node_kore): $(node_files)
- $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) --backend llvm \
- --syntax-module $(SYNTAX_MODULE) $(node_dir)/$(MAIN_DEFN_FILE).k \
- --directory $(node_dir) -I $(node_dir) -I $(node_dir) \
- --hook-namespaces "KRYPTO BLOCKCHAIN" \
- --no-llvm-kompile \
- $(KOMPILE_OPTS)
+# Haskell
-$(node_dir)/$(MAIN_DEFN_FILE)-kompiled/plugin/proto/msg.pb.cc: $(PLUGIN_SUBMODULE)/plugin/proto/msg.proto
- @mkdir -p $(node_dir)/$(MAIN_DEFN_FILE)-kompiled/plugin
- protoc --cpp_out=$(node_dir)/$(MAIN_DEFN_FILE)-kompiled/plugin -I $(PLUGIN_SUBMODULE)/plugin $(PLUGIN_SUBMODULE)/plugin/proto/msg.proto
-
-$(node_kompiled): $(node_kore) $(node_dir)/$(MAIN_DEFN_FILE)-kompiled/plugin/proto/msg.pb.cc $(libff_out)
- @mkdir -p $(DEFN_DIR)/vm
- cd $(DEFN_DIR)/vm && cmake $(CURDIR)/cmake/node -DCMAKE_BUILD_TYPE=${SEMANTICS_BUILD_TYPE} -DCMAKE_INSTALL_PREFIX=${INSTALL_PREFIX} && $(MAKE)
+$(haskell_kompiled): $(haskell_files)
+ kompile --debug --main-module $(MAIN_MODULE) --backend haskell --hook-namespaces KRYPTO \
+ --syntax-module $(SYNTAX_MODULE) $(haskell_dir)/$(MAIN_DEFN_FILE).k \
+ --directory $(haskell_dir) -I $(haskell_dir) \
+ $(KOMPILE_OPTS)
-# Web3 Backend
+# Web3
$(web3_kore): $(web3_files)
- $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) --backend llvm \
- --syntax-module $(SYNTAX_MODULE) $(web3_dir)/$(MAIN_DEFN_FILE).k \
- --directory $(web3_dir) -I $(web3_dir) \
- --hook-namespaces "KRYPTO JSON" \
- --no-llvm-kompile \
- $(KOMPILE_OPTS)
+ kompile --debug --main-module $(MAIN_MODULE) --backend llvm \
+ --syntax-module $(SYNTAX_MODULE) $(web3_dir)/$(MAIN_DEFN_FILE).k \
+ --directory $(web3_dir) -I $(web3_dir) \
+ --hook-namespaces "KRYPTO JSON" \
+ --no-llvm-kompile \
+ $(KOMPILE_OPTS)
$(web3_kompiled): $(web3_kore) $(libff_out)
@mkdir -p $(web3_dir)/build
- cd $(web3_dir)/build && cmake $(CURDIR)/cmake/client -DCMAKE_BUILD_TYPE=${SEMANTICS_BUILD_TYPE} -DCMAKE_INSTALL_PREFIX=${INSTALL_PREFIX} && $(MAKE)
+ cd $(web3_dir)/build && cmake $(CURDIR)/cmake/client -DCMAKE_BUILD_TYPE=$(SEMANTICS_BUILD_TYPE) && $(MAKE)
+
+# Standalone
+
+STANDALONE_KOMPILE_OPTS := -L$(LOCAL_LIB) -I$(K_RELEASE)/include/kllvm \
+ $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp \
+ $(PLUGIN_SUBMODULE)/plugin-c/blake2.cpp \
+ -g -std=c++14 -lff -lcryptopp -lsecp256k1
-# LLVM Backend
+ifeq ($(UNAME_S),Linux)
+ STANDALONE_KOMPILE_OPTS += -lprocps
+endif
$(llvm_kompiled): $(llvm_files) $(libff_out)
- $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) --backend llvm \
- --syntax-module $(SYNTAX_MODULE) $(llvm_dir)/$(MAIN_DEFN_FILE).k \
- --directory $(llvm_dir) -I $(llvm_dir) -I $(llvm_dir) \
- --hook-namespaces KRYPTO \
- $(KOMPILE_OPTS) \
- -ccopt $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp \
- -ccopt $(PLUGIN_SUBMODULE)/plugin-c/blake2.cpp \
- -ccopt -g -ccopt -std=c++14 \
- -ccopt -L$(LIBRARY_PATH) \
- -ccopt -lff -ccopt -lcryptopp -ccopt -lsecp256k1 $(addprefix -ccopt ,$(LINK_PROCPS))
+ kompile --debug --main-module $(MAIN_MODULE) --backend llvm \
+ --syntax-module $(SYNTAX_MODULE) $(llvm_dir)/$(MAIN_DEFN_FILE).k \
+ --directory $(llvm_dir) -I $(llvm_dir) \
+ --hook-namespaces KRYPTO \
+ $(KOMPILE_OPTS) \
+ $(addprefix -ccopt ,$(STANDALONE_KOMPILE_OPTS))
# Installing
# ----------
@@ -318,12 +292,6 @@ KPROVE_OPTIONS :=
test-all: test-all-conformance test-prove test-interactive test-parse
test: test-conformance test-prove test-interactive test-parse
-split-tests: tests/ethereum-tests/make.timestamp
-
-tests/%/make.timestamp:
- git submodule update --init -- tests/$*
- touch $@
-
# Generic Test Harnesses
tests/ethereum-tests/VMTests/%: KEVM_MODE=VMTESTS
@@ -366,7 +334,8 @@ tests/specs/functional/%.prove: TEST_SYMBOLIC_BACKEND=haskell
tests/specs/examples/%.prove: TEST_SYMBOLIC_BACKEND=haskell
tests/specs/functional/storageRoot-spec.k.prove: TEST_SYMBOLIC_BACKEND=java
-tests/specs/functional/lemmas-spec.k.prove: TEST_SYMBOLIC_BACKEND=java
+tests/specs/functional/lemmas-no-smt-spec.k.prove: KPROVE_OPTIONS+=--haskell-backend-command "kore-exec --smt=none"
+tests/specs/erc20/hkg/totalSupply-spec.k.prove: TEST_SYMBOLIC_BACKEND=haskell
tests/%.prove: tests/%
$(TEST) prove $(TEST_OPTIONS) --backend $(TEST_SYMBOLIC_BACKEND) $< $(KPROVE_MODULE) --format-failures $(KPROVE_OPTIONS) \
@@ -374,6 +343,13 @@ tests/%.prove: tests/%
$(CHECK) $@.out $@.expected
rm -rf $@.out
+tests/specs/imp-specs/%.prove: tests/specs/imp-specs/%
+ $(TEST) prove $(TEST_OPTIONS) --backend-dir $(specs_dir) \
+ --backend $(TEST_SYMBOLIC_BACKEND) $< $(KPROVE_MODULE) --format-failures $(KPROVE_OPTIONS) \
+ --concrete-rules $(shell cat $(dir $@)concrete-rules.txt | tr '\n' ',') > $@.out || \
+ $(CHECK) $@.out $@.expected
+ rm -rf $@.out
+
tests/%.search: tests/%
$(TEST) search $(TEST_OPTIONS) --backend $(TEST_SYMBOLIC_BACKEND) $< " EVMC_INVALID_INSTRUCTION " > $@-out
$(CHECK) $@-out $@-expected
@@ -443,14 +419,16 @@ prove_opcodes_tests := $(filter-out $(prove_failing_tests), $(wildcard $(prov
prove_erc20_tests := $(filter-out $(prove_failing_tests), $(wildcard $(prove_specs_dir)/erc20/*/*-spec.k))
prove_bihu_tests := $(filter-out $(prove_failing_tests), $(wildcard $(prove_specs_dir)/bihu/*-spec.k))
prove_examples_tests := $(filter-out $(prove_failing_tests), $(wildcard $(prove_specs_dir)/examples/*-spec.k))
+prove_imp_specs_tests := $(filter-out $(prove_failing_tests), $(wildcard $(prove_specs_dir)/imp-specs/*-spec.k))
-test-prove: test-prove-benchmarks test-prove-functional test-prove-opcodes test-prove-erc20 test-prove-bihu test-prove-examples
+test-prove: test-prove-benchmarks test-prove-functional test-prove-opcodes test-prove-erc20 test-prove-bihu test-prove-examples test-prove-imp-specs
test-prove-benchmarks: $(prove_benchmarks_tests:=.prove)
test-prove-functional: $(prove_functional_tests:=.prove)
test-prove-opcodes: $(prove_opcodes_tests:=.prove)
test-prove-erc20: $(prove_erc20_tests:=.prove)
test-prove-bihu: $(prove_bihu_tests:=.prove)
test-prove-examples: $(prove_examples_tests:=.prove)
+test-prove-imp-specs: $(prove_imp_specs_tests:=.prove)
test-failing-prove: $(prove_failing_tests:=.prove)
@@ -504,6 +482,4 @@ media-pdf: $(patsubst %, media/%.pdf, $(media_pdfs))
metropolis-theme: $(BUILD_DIR)/media/metropolis/beamerthememetropolis.sty
$(BUILD_DIR)/media/metropolis/beamerthememetropolis.sty:
- git submodule update --init -- $(dir $@)
cd $(dir $@) && $(MAKE)
-
diff --git a/README.md b/README.md
index 4ea471418f..745c492b50 100644
--- a/README.md
+++ b/README.md
@@ -21,15 +21,18 @@ Repository Structure
The following files constitute the KEVM semantics:
- [krypto.md](krypto.md) sets up some basic cryptographic primitives.
-- [data.md](data.md) provides the (functional) data of EVM (256 bit words, wordstacks, etc...).
- [network.md](network.md) provides the status codes which are reported to an Ethereum client on execution exceptions.
+- [json.md](json.md) is an implementation of the JSON format in K.
+- [evm-types.md](evm-types.md) provides the (functional) data of EVM (256 bit words, wordstacks, etc...).
+- [serialization.md](serialization.md) provides helpers for parsing and unparsing data (hex strings, recursive-length prefix, merkle trees, etc.).
- [evm.md](evm.md) is the main KEVM semantics, containing the configuration and transition rules of EVM.
These additional files extend the semantics to make the repository more useful:
-- [driver.md](driver.md) is an execution harness for KEVM, providing a simple language for describing tests/programs.
- [edsl.md](edsl.md) defines high-level notations of [eDSL], a domain-specific language for EVM specifications, for formal verification of EVM bytecode using [K Reachability Logic Prover].
-- [evm-node.md](evm-node.md) is the protobuf interface that an external Ethereum client can connect to for using KEVM as the execution engine.
+- [state-loader.md](state-loader.md) provides common functionality between driver and web3 for EVM initialization and setup.
+- [driver.md](driver.md) is an execution harness for KEVM, providing a simple language for describing tests/programs.
+- [web3.md](web3.md) is a web3 rpc server.
Installing/Building
-------------------
@@ -49,16 +52,17 @@ The following are needed for building/running KEVM:
- GNU [libmpfr](http://www.mpfr.org/) and [libtool](https://www.gnu.org/software/libtool/).
- Java 8 JDK (eg. [OpenJDK](http://openjdk.java.net/))
+For the exact dependencies check the Dockerfile, but they should look something like this.
On Ubuntu >= 18.04 (for example):
```sh
-sudo apt install \
- autoconf bison clang++-8 clang-8 cmake curl flex gcc git \
- libboost-test-dev libgmp-dev libjemalloc-dev libmpfr-dev \
- libprocps-dev libprotobuf-dev libsecp256k1-dev libtool \
- libyaml-dev libz3-dev lld-8 llvm-8 llvm-8-tools make maven \
- openjdk-11-jdk pandoc pkg-config protobuf-compiler z3 \
- zlib1g-dev
+sudo apt-get install --yes \
+ autoconf bison clang-8 cmake curl flex gcc jq libboost-test-dev \
+ libcrypto++-dev libffi-dev libgflags-dev libjemalloc-dev libmpfr-dev \
+ libprocps-dev libsecp256k1-dev libssl-dev libtool libyaml-dev \
+ lld-8 llvm-8-tools make maven netcat-openbsd openjdk-11-jdk \
+ pandoc pkg-config python3 python-pygments python-recommonmark \
+ python-sphinx rapidjson-dev time zlib1g-dev
```
On Ubuntu < 18.04, you'll need to skip `libsecp256k1-dev` and instead build it from source (via our `Makefile`):
@@ -103,39 +107,21 @@ export PATH=$HOME/.local/bin:$PATH
### Build K Dependency
-Get the submodules:
-
-```sh
-git submodule update --init --recursive
-```
-
-And finally build the repository specific dependencies:
-
-```sh
-make RELEASE=1 deps
-```
-If you are a developer, you probably should omit `RELEASE` from the above commands unless you are testing performance, as the build is somewhat slower.
-
-On Arch, instead do:
+The `Makefile` and `kevm` will work with either a (i) globally installed K, or (ii) the submodule built K.
+If you want to use the submodule, follow these instructions, then get the submodules and build the repository dependencies:
```sh
-make LIBFF_CC=clang LIBFF_CXX=clang++ RELEASE=1 deps
+git submodule update --init --recursive -- deps/k
+make deps
```
### Building
-Finally, you can install repository specific dependencies and build the semantics:
-
-```sh
-make build RELEASE=1
-```
-
-You can also build specific backends as so:
+Finally, you can build the semantics (after getting the plugin and tangle submodule dependencies):
```sh
-make build-haskell
-make build-llvm RELEASE=1
-make build-java
+git submodule update --init --recursive -- deps/plugin deps/pandoc-tangle
+make build
```
Example Usage
diff --git a/cmake/client/CMakeLists.txt b/cmake/client/CMakeLists.txt
index 13f700d7c1..5dd5b97232 100644
--- a/cmake/client/CMakeLists.txt
+++ b/cmake/client/CMakeLists.txt
@@ -1,6 +1,7 @@
cmake_minimum_required (VERSION 3.4)
list(APPEND CMAKE_MODULE_PATH "$ENV{K_RELEASE}/cmake")
+list(APPEND CMAKE_MODULE_PATH "$ENV{K_RELEASE}/lib/cmake/kframework")
include(LLVMKompilePrelude)
project (KevmClient CXX)
@@ -9,7 +10,7 @@ set(KOMPILE_USE_MAIN "library")
set(TARGET_NAME "kevm-client")
add_executable(kevm-client
- $ENV{PLUGIN_SUBMODULE}/vm-c/init.cpp
+ $ENV{PLUGIN_SUBMODULE}/client-c/init.cpp
$ENV{PLUGIN_SUBMODULE}/client-c/main.cpp
$ENV{PLUGIN_SUBMODULE}/client-c/json.cpp
$ENV{PLUGIN_SUBMODULE}/plugin-c/crypto.cpp
@@ -21,14 +22,14 @@ endif()
target_include_directories(kevm-client
PUBLIC $ENV{PLUGIN_SUBMODULE}/plugin-c
- PUBLIC $ENV{PLUGIN_SUBMODULE}/vm-c
- PUBLIC $ENV{PLUGIN_SUBMODULE}/deps/websocketpp
+ PUBLIC $ENV{PLUGIN_SUBMODULE}/deps/cpp-httplib
+ PUBLIC $ENV{K_RELEASE}/include/kllvm
PUBLIC ${CMAKE_SOURCE_DIR}/..)
target_compile_options(kevm-client
PUBLIC $ENV{LLVM_KOMPILE_OPTS}
PUBLIC -Wall -Werror -Wno-unknown-warning-option)
target_link_libraries(kevm-client
- ff gmp ${LINK_PROCPS} cryptopp secp256k1 gflags boost_system
+ ff gmp ${LINK_PROCPS} cryptopp secp256k1 gflags
)
include(LLVMKompile)
diff --git a/cmake/node/CMakeLists.txt b/cmake/node/CMakeLists.txt
deleted file mode 100644
index 824b874d2a..0000000000
--- a/cmake/node/CMakeLists.txt
+++ /dev/null
@@ -1,40 +0,0 @@
-cmake_minimum_required (VERSION 3.4)
-
-list(APPEND CMAKE_MODULE_PATH "$ENV{K_RELEASE}/cmake")
-include(LLVMKompilePrelude)
-project (KevmVm CXX)
-
-set(KOMPILED_DIR $ENV{node_dir}/$ENV{MAIN_DEFN_FILE}-kompiled)
-set(KOMPILE_USE_MAIN "library")
-set(TARGET_NAME "kevm-vm")
-
-link_directories(AFTER SYSTEM $ENV{LIBRARY_PATH})
-
-add_executable(kevm-vm
- $ENV{PLUGIN_SUBMODULE}/vm-c/init.cpp
- $ENV{PLUGIN_SUBMODULE}/vm-c/main.cpp
- $ENV{PLUGIN_SUBMODULE}/vm-c/vm.cpp
- $ENV{PLUGIN_SUBMODULE}/plugin-c/blake2.cpp
- $ENV{PLUGIN_SUBMODULE}/plugin-c/blockchain.cpp
- $ENV{PLUGIN_SUBMODULE}/plugin-c/crypto.cpp
- $ENV{PLUGIN_SUBMODULE}/plugin-c/world.cpp
- $ENV{node_dir}/$ENV{MAIN_DEFN_FILE}-kompiled/plugin/proto/msg.pb.cc
- $ENV{PLUGIN_SUBMODULE}/vm-c/kevm/semantics.cpp)
-
-if(UNIX AND NOT APPLE)
- set(LINK_PROCPS procps)
-endif()
-
-target_include_directories(kevm-vm
- PUBLIC $ENV{PLUGIN_SUBMODULE}/plugin-c
- PUBLIC $ENV{node_dir}/$ENV{MAIN_DEFN_FILE}-kompiled/plugin
- PUBLIC $ENV{PLUGIN_SUBMODULE}/vm-c
- PUBLIC $ENV{PLUGIN_SUBMODULE}/vm-c/kevm
- PUBLIC ${CMAKE_SOURCE_DIR}/..)
-target_compile_options(kevm-vm
- PUBLIC $ENV{LLVM_KOMPILE_OPTS}
- PUBLIC -Wall -Werror)
-target_link_libraries(kevm-vm
- ff protobuf gmp ${LINK_PROCPS} cryptopp secp256k1)
-
-include(LLVMKompile)
diff --git a/data.md b/data.md
index b592193fbf..b073e389ad 100644
--- a/data.md
+++ b/data.md
@@ -16,7 +16,7 @@ module EVM-DATA
imports STRING-BUFFER
imports MAP-SYMBOLIC
imports COLLECTIONS
- imports JSON
+ imports JSON-EXT
```
```{.k .concrete .bytes}
diff --git a/deps/k b/deps/k
index 280480e6e4..5396aae9ab 160000
--- a/deps/k
+++ b/deps/k
@@ -1 +1 @@
-Subproject commit 280480e6e415f4f2c570198ee577f9dbeec33fcb
+Subproject commit 5396aae9abfd2a6899207ac4e8fba1dfe6681f49
diff --git a/deps/plugin b/deps/plugin
index 1d4f18a463..1081ab8770 160000
--- a/deps/plugin
+++ b/deps/plugin
@@ -1 +1 @@
-Subproject commit 1d4f18a463aa35b4f0cac8dbdca3adacf58305f9
+Subproject commit 1081ab8770979703830f0f867ca105b2480f9e50
diff --git a/driver.md b/driver.md
index f5a3ce7cb6..be4092a3ce 100644
--- a/driver.md
+++ b/driver.md
@@ -39,25 +39,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
```k
syntax JSON ::= ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
// -----------------------------------------------------------------------------
-
- syntax JSONs ::= #sortJSONs ( JSONs ) [function]
- | #sortJSONs ( JSONs , JSONs ) [function, klabel(#sortJSONsAux)]
- // -------------------------------------------------------------------------------
- rule #sortJSONs(JS) => #sortJSONs(JS, .JSONs)
- rule #sortJSONs(.JSONs, LS) => LS
- rule #sortJSONs(((KEY : VAL) , REST), LS) => #insertJSONKey((KEY : VAL), #sortJSONs(REST, LS))
-
- syntax JSONs ::= #insertJSONKey ( JSON , JSONs ) [function]
- // -----------------------------------------------------------
- rule #insertJSONKey( JS , .JSONs ) => JS , .JSONs
- rule #insertJSONKey( (KEY : VAL) , ((KEY' : VAL') , REST) ) => (KEY : VAL) , (KEY' : VAL') , REST requires KEY (KEY' : VAL') , #insertJSONKey((KEY : VAL) , REST) requires KEY >=String KEY'
-
- syntax Bool ::= #isSorted ( JSONs ) [function]
- // ----------------------------------------------
- rule #isSorted( .JSONs ) => true
- rule #isSorted( KEY : _ ) => true
- rule #isSorted( (KEY : _) , (KEY' : VAL) , REST ) => KEY <=String KEY' andThenBool #isSorted((KEY' : VAL) , REST)
```
### Driving Execution
@@ -89,7 +70,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
rule startTx => #finalizeBlock ...
.List
- rule startTx => loadTx(#sender(TN, TP, TG, TT, TV, #unparseByteStack(DATA), TW, TR, TS)) ...
+ rule startTx => loadTx(#sender(TN, TP, TG, TT, TV, #unparseByteStack(DATA), TW, TR, TS, CID)) ...
+ CID
ListItem(TXID:Int) ...
TXID
@@ -107,8 +89,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
syntax EthereumCommand ::= loadTx ( Account )
// ---------------------------------------------
rule loadTx(ACCTFROM)
- => #loadAccount #newAddr(ACCTFROM, NONCE)
- ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
+ => #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
~> #finishTx ~> #finalizeTx(false) ~> startTx
...
@@ -137,9 +118,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
_ => SetItem(MINER)
rule loadTx(ACCTFROM)
- => #loadAccount ACCTTO
- ~> #lookupCode ACCTTO
- ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
+ => #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
~> #finishTx ~> #finalizeTx(false) ~> startTx
...
@@ -213,7 +192,11 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
syntax EthereumCommand ::= "failure" String | "success"
// -------------------------------------------------------
- rule success => . ... _ => 0 _ => SUCCESS
+ rule success => . ...
+ _ => 0
+ _ => SUCCESS
+ _ => 0
+
rule failure _ => . ...
rule #halt ~> failure _ => . ...
```
@@ -229,7 +212,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
// -------------------------------------
rule run { .JSONs } => . ...
rule run { TESTID : { TEST:JSONs } , TESTS }
- => run ( TESTID : { #sortJSONs(TEST) } )
+ => run ( TESTID : { qsortJSONs(TEST) } )
~> #if #hasPost?( { TEST } ) #then .K #else exception #fi
~> clear
~> run { TESTS }
@@ -316,7 +299,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
- `driver.md` specific handling of state-loader commands
-```{.k .standalone}
+```k
rule load "account" : { ACCTID : ACCT } => loadAccount ACCTID ACCT ...
rule loadAccount _ { "balance" : ((VAL:String) => #parseWord(VAL)), _ } ...
@@ -353,8 +336,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule check DATA : [ { TEST } , REST ] => check DATA : { TEST } ~> check DATA : [ REST ] ...
requires DATA =/=String "transactions"
- rule check (KEY:String) : { JS:JSONs => #sortJSONs(JS) } ...
- requires KEY in (SetItem("callcreates")) andBool notBool #isSorted(JS)
+ rule check (KEY:String) : { JS:JSONs => qsortJSONs(JS) } ...
+ requires KEY in (SetItem("callcreates")) andBool notBool sortedJSONs(JS)
rule check TESTID : { "post" : POST } => check "account" : POST ~> failure TESTID ...
rule check "account" : { ACCTID:Int : { KEY : VALUE , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } ...
diff --git a/edsl.md b/edsl.md
index 2935c1772e..2e50e2c5ad 100644
--- a/edsl.md
+++ b/edsl.md
@@ -54,9 +54,11 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
syntax ByteArray ::= #abiCallData ( String , TypedArgs ) [function]
// -------------------------------------------------------------------
- rule #abiCallData( FNAME , ARGS )
- => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8))
- ++ #encodeArgs(ARGS)
+ rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) ++ #encodeArgs(ARGS)
+
+ syntax ByteArray ::= #signatureCallData ( String, TypedArgs ) [function]
+ // ------------------------------------------------------------------------
+ rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8))
syntax String ::= #generateSignature ( String, TypedArgs ) [function]
| #generateSignatureArgs ( TypedArgs ) [function]
@@ -183,6 +185,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8)))
[concrete]
+ rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #rangeBytes(SIZE, DATA) #Equals true} [anywhere, simplification]
+
syntax Int ::= #getValue ( TypedArg ) [function]
// ------------------------------------------------
rule #getValue(#uint160( DATA )) => DATA
diff --git a/evm-imp-specs.md b/evm-imp-specs.md
new file mode 100644
index 0000000000..6970a576ee
--- /dev/null
+++ b/evm-imp-specs.md
@@ -0,0 +1,144 @@
+Scripting language for imperative specifications (SOLAR-style)
+==============================================================
+
+```k
+requires "evm.k"
+
+module EVM-IMP-SPECS
+ imports ID
+ imports EVM
+
+ configuration
+
+
+ .Map
+
+```
+
+Core specification language
+---------------------------
+
+```k
+ syntax EthereumCommand ::= "#assert" Exp [strict]
+ | "#assertFailure" Exp
+ rule #assert R:Bool => . ...
+ requires R
+
+ rule #assert R:Bool => #assertFailure R ...
+ requires notBool R
+
+ syntax EthereumCommand ::= "#assume" Exp [strict]
+
+ //Adapted from driver.md `failure`
+ syntax EthereumCommand ::= "#takeHalt" String
+ // ---------------------------------------------
+ rule #takeHalt _ => . ...
+ rule #halt ~> #takeHalt _ => . ...
+
+ //Shortcut for #mkCall and required setup
+ syntax EthereumCommand ::= "#mkCallShortcut" Id Int Int ByteArray Id
+ rule #mkCallShortcut V_CONF_BACKUP CALLER_ID ACCT_ID ARGS V_SAVEOUT_ID
+ => #restoreEthereum V_CONF_BACKUP
+ ~> #mkCall CALLER_ID ACCT_ID ACCT_ID PARSEDCODE 0 ARGS false
+ ~> #takeHalt "failure"
+ ~> #saveOutput V_SAVEOUT_ID
+ ...
+
+ ACCT_ID
+ PARSEDCODE
+
+ //Dummy command at the beginning of to ensure execution doesn't start with a spec rule
+ syntax EthereumCommand ::= "#dummy"
+ rule #dummy => . ...
+```
+
+Configuration access commands
+-----------------------------
+
+```k
+ syntax EthereumCommand ::= "#saveEthereum" Id
+ rule #saveEthereum X => . ...
+ ETH
+ VARS => VARS[X <- ETH]
+
+ syntax EthereumCommand ::= "#restoreEthereum" Id
+ rule #restoreEthereum X => . ...
+ ( _ => ETH )
+ ... X |-> ETH ...
+
+ syntax EthereumCommand ::= "#saveOutput" Id
+ rule #saveOutput X => . ...
+
+ VARS => VARS[X <- OUT]
+
+ syntax EthereumCommand ::= "#saveStorage" Int Id
+ rule #saveStorage ACCT_ID X => . ...
+ ACCT_ID
+ S
+ VARS => VARS[X <- S]
+
+ syntax EthereumCommand ::= "#saveLog" Id
+ rule #saveLog X => . ...
+ L
+ VARS => VARS[X <- L]
+
+ syntax EthereumCommand ::= "#saveRefund" Id
+ rule #saveRefund X => . ...
+ R
+ VARS => VARS[X <- R]
+```
+
+Specification expression language
+---------------------------------
+
+```k
+ syntax KResult ::= ByteArray | StatusCode | List | Map
+
+ syntax Exp ::= Exp "==S" Exp [seqstrict]
+ | Exp "=/=S" Exp [seqstrict]
+ | Exp "+List" Exp [seqstrict]
+ | KResult
+
+ rule R1:KResult ==S R2:KResult => R1 ==K R2 ...
+ rule R1:KResult =/=S R2:KResult => R1 =/=K R2 ...
+ rule L1:List +List L2:List => L1 L2 ...
+
+ // Boolean expressions
+ syntax Exp ::= Exp "&&S" Exp [seqstrict, left]
+ > Exp "||S" Exp [seqstrict, left]
+
+ rule R1:Bool &&S R2:Bool => R1 andBool R2 ...
+ rule R1:Bool ||S R2:Bool => R1 orBool R2 ...
+
+ // Configuration access and other helpers
+ syntax Exp ::= "#getStatusCode"
+ | "#getOutput"
+ | "#getLog"
+ | "#getRefund"
+ | #getStorage ( Int )
+ | #var( Id )
+ | #sizeByteArrayExp ( Exp ) [strict]
+
+ rule #getStatusCode => SC ...
+ SC
+
+ rule #getOutput => OUT ...
+
+
+ rule #getLog => L ...
+ L
+
+ rule #getRefund => R ...
+ R
+
+ rule #getStorage(ACCT_ID) => S ...
+ ACCT_ID
+ S
+
+ rule #var(X) => VARS[X] ...
+ VARS
+
+ rule #sizeByteArrayExp(WS:ByteArray) => #sizeByteArray(WS) ...
+
+endmodule
+```
diff --git a/evm-node.md b/evm-node.md
deleted file mode 100644
index f522260956..0000000000
--- a/evm-node.md
+++ /dev/null
@@ -1,266 +0,0 @@
-EVM Integration with Production Client
-======================================
-
-Contained in this file is glue code needed in order to enable the ability to use KEVM as a VM for an actual Ethereum node.
-
-```{.k .node}
-requires "evm.k"
-
-module EVM-NODE
- imports EVM
- imports K-REFLECTION
- imports COLLECTIONS
- imports BYTES
-```
-
-### State loading operations.
-
-In order to enable scalable execution of transactions on an entire blockchain, it is necessary to avoid serializing/deserializing the entire state of all accounts when constructing the initial configuration for KEVM.
-To do this, we assume that accounts not present in the `` cell might not exist and need to be loaded on each access.
-We also defer loading of storage entries and the actual code byte string until it is needed.
-Because the same account may be loaded more than once, implementations of this interface are expected to cache the actual query to the Ethereum client.
-
-- `#unloaded` represents the code of an account that has not had its code loaded yet. Unloaded code may not be empty.
-- Empty code is detected without lazy evaluation by means of checking the code hash, and therefore will always be represented in the `` cell as `.WordStack`.
-
-```{.k .node}
- syntax AccountCode ::= #unloaded(Int)
-```
-
-- `#getBalance` returns the balance of an account that exists based on its integer address.
-- `#getNonce` returns the nonce of an account that exists based on its integer address.
-- `#isCodeEmpty` returns true if the code hash of the account is equal to the hash of the empty string, and false otherwise.
-- `#accountExists` returns true if the account is present in the state trie for the current block, and false otherwise.
-
-```{.k .node}
- syntax Int ::= #getBalance ( Int ) [function, hook(BLOCKCHAIN.getBalance)]
- | #getNonce ( Int ) [function, hook(BLOCKCHAIN.getNonce)]
- | #getCodeHash ( Int ) [function, hook(BLOCKCHAIN.getCodeHash)]
- // -----------------------------------------------------------------------------
-
- syntax Bool ::= #isCodeEmpty ( Int ) [function, hook(BLOCKCHAIN.isCodeEmpty)]
- | #accountExists ( Int ) [function, hook(BLOCKCHAIN.accountExists)]
- // ---------------------------------------------------------------------------------
-```
-
-- `#loadAccount` loads an account's balance and nonce if it exists, and leaves the code and storage unloaded, except if the code is empty, in which case the code is fully loaded.
- If the account does not exist, it does nothing.
-
-```{.k .node}
- rule #loadAccount ACCT => . ...
- ACCTS (.Set => SetItem(ACCT))
-
- ( .Bag
- =>
- ACCT
- #getBalance(ACCT)
- #if #isCodeEmpty(ACCT) #then .ByteArray #else #unloaded(#getCodeHash(ACCT)) #fi
- .Map
- .Map
- #getNonce(ACCT)
-
- )
- ...
-
- requires notBool ACCT in ACCTS andBool #accountExists(ACCT)
-
- rule #loadAccount ACCT => . ...
- ACCTS
- requires ACCT in ACCTS orBool notBool #accountExists(ACCT)
-```
-
-- `#getStorageData` loads the value for a single storage key of a specified account by its address and storage offset.
- If the storage key has already been loaded or the account does not exist, it does nothing.
-
-```{.k .node}
- syntax Int ::= #getStorageData ( Int , Int ) [function, hook(BLOCKCHAIN.getStorageData)]
- // ----------------------------------------------------------------------------------------
- rule #lookupStorage ACCT INDEX => . ...
-
- ACCT
- STORAGE => STORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ]
- ORIGSTORAGE => ORIGSTORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ]
- ...
-
- requires notBool INDEX in_keys(STORAGE)
-
- rule #lookupStorage ACCT INDEX => . ...
-
- ACCT
- STORAGE:Map
- ...
-
- requires INDEX in_keys(STORAGE)
-
- rule #lookupStorage ACCT _ => . ...
- requires notBool #accountExists(ACCT)
-```
-
-- `#getCode` loads the code for a specified account by its address. If the code has already been loaded, it does nothing.
- If the account does not exist, it also does nothing.
-
-```{.k .node}
- syntax String ::= #getCode ( Int ) [function, hook(BLOCKCHAIN.getCode)]
- // -----------------------------------------------------------------------
- rule #lookupCode ACCT => . ...
-
- ACCT
- #unloaded(_) => #parseByteStackRaw(#getCode(ACCT))
- ...
-
-
- rule #lookupCode ACCT => . ...
-
- ACCT
- _:ByteArray
- ...
-
-
- rule #lookupCode ACCT => . ...
- requires notBool #accountExists(ACCT)
-```
-
-- `#getBlockhash(N)` returns the blockhash of the Nth most recent block, up to a maximum of 256 blocks.
- It is used in the implementation of the BLOCKHASH instruction as seen below.
-
-```{.k .node}
- syntax Int ::= #getBlockhash ( Int ) [function, hook(BLOCKCHAIN.getBlockhash)]
- // ------------------------------------------------------------------------------
- rule BLOCKHASH N => #getBlockhash(N) ~> #push ... NORMAL requires N >=Int 0 andBool N BLOCKHASH N => 0 ~> #push ... NORMAL requires N =Int 256
-```
-
-```{.k .node}
- rule EXTCODEHASH ACCT => HASH ~> #push ...
-
- ACCT
- #unloaded(HASH)
- NONCE
- BAL
- ...
-
-```
-
-### Transaction Execution
-
-- `runVM` takes all the input state of a transaction and the current block header and executes the transaction according to the specified state, relying on the above loading operations for access to accounts and block hashes.
- The signature of this function must match the signature expected by VM.ml in the blockchain-k-plugin.
-
-```{.k .node}
- syntax EthereumSimulation ::= runVM ( iscreate: Bool , to: Int , from: Int , code: String , args: String , value: Int , gasprice: Int
- , gas: Int , beneficiary: Int , difficulty: Int , number: Int , gaslimit: Int , timestamp: Int , unused: String ) [symbol]
- // ----------------------------------------------------------------------------------------------------------------------------------------------------------------------
- rule (.K => #loadAccount ACCTFROM) ~> runVM(... from: ACCTFROM) ...
- .Set
-
- rule runVM(true, _, ACCTFROM, _, ARGS, VALUE, GPRICE, GAVAIL, CB, DIFF, NUMB, GLIMIT, TS, _)
- => #loadAccount #newAddr(ACCTFROM, NONCE -Int 1)
- ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE -Int 1) VALUE #parseByteStackRaw(ARGS)
- ~> #codeDeposit #newAddr(ACCTFROM, NONCE -Int 1)
- ~> #endCreate
- ...
-
- SCHED
- _ => GPRICE
- _ => GAVAIL
- _ => ACCTFROM
- _ => -1
- _ => CB
- _ => DIFF
- _ => NUMB
- _ => GLIMIT
- _ => TS
-
- ACCTFROM
- NONCE
- ...
-
- _ => SetItem(CB)
- ACCTS
- requires ACCTFROM in ACCTS
-
- rule runVM(false, ACCTTO, ACCTFROM, _, ARGS, VALUE, GPRICE, GAVAIL, CB, DIFF, NUMB, GLIMIT, TS, _)
- => #loadAccount ACCTTO
- ~> #lookupCode ACCTTO
- ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE #parseByteStackRaw(ARGS) false
- ~> #endVM
- ...
-
- SCHED
- _ => GPRICE
- _ => GAVAIL
- _ => ACCTFROM
- _ => -1
- _ => CB
- _ => DIFF
- _ => NUMB
- _ => GLIMIT
- _ => TS
- _ => SetItem(CB)
- ACCTS
- requires ACCTFROM in ACCTS
-```
-
-- `#endCreate` and `#endVM` clean up after the transaction finishes and store the return status code of the top level call frame on the top of the `` cell.
-
-```{.k .node}
- syntax KItem ::= "#endVM" | "#endCreate"
- // ----------------------------------------
- rule _:ExceptionalStatusCode
- #halt ~> #endVM => #popCallStack ~> #popWorldState ~> 0
-
-
- rule EVMC_REVERT
- #halt ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0
- GAVAIL
-
- rule EVMC_SUCCESS
- #halt ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1
- GAVAIL
-
- rule #endCreate => W ... W : WS
-```
-
-### Primitive operations expected to exist by the blockchain-k-plugin
-
-- `vmResult` represents the extracted information about the world state after the transaction finishes.
- Its signature must match the signature expected by VM.ml in the blockchain-k-plugin.
-- `extractConfig` takes a final configuration after rewriting and extracts a `vmResult` from it in order to abstract away configuration structure from the postprocessing done by the blockchain-k-plugin.
-
-```{.k .node}
- syntax KItem ::= vmResult ( return: String , gas: Int , refund: Int , status: Int , selfdestruct: Set , logs: List , AccountsCell , touched: Set , statusCode: String )
- syntax KItem ::= extractConfig() [function, symbol]
- // ---------------------------------------------------
- rule [[ extractConfig() => vmResult(#unparseByteStack(OUT), GAVAIL, REFUND, STATUS, SD, LOGS, ACCTS , TOUCHED, StatusCode2String(STATUSCODE)) ]]
-
- GAVAIL
- REFUND
- STATUS:Int
- SD
- LOGS
- ACCTS
- TOUCHED
- STATUSCODE
-```
-
-- `contractBytes` takes the contents of the `` cell and returns its binary representation as a String.
-
-```{.k .node}
- syntax String ::= contractBytes(AccountCode) [function, symbol]
- // ---------------------------------------------------------------
- rule contractBytes(WS) => #unparseByteStack(WS)
-```
-
-The following are expected to exist in the client, but are already defined in [data.md].
-
-- `accountEmpty` takes the contents of the `` cell, the contents of the `` cell, and the contents of the `` cell and returns true if the account is empty according to the semantics of EIP161 (i.e., empty code zero balance zero nonce).
-- `unparseByteStack` takes a WordStack and returns the corresponding byte String.
-- `initKevmCell` is the top cell initializer used to construct an initial configuration.
- The configuration is expected to have `$MODE`, `$PGM`, and `$SCHEDULE` parameters.
-- `logEntry` is an entry in the log data created by a transaction.
- It is expected to consist of an Int address, a List of Int topics, and a WordStack of data.
-- `NORMAL` is the value of `$MODE` used by actual transaction execution.
-
-```{.k .node}
-endmodule
-```
diff --git a/evm-types.md b/evm-types.md
index 866b83b3de..81b8e73888 100644
--- a/evm-types.md
+++ b/evm-types.md
@@ -99,6 +99,7 @@ These can be used for pattern-matching on the LHS of rules as well (`macro` attr
rule #rangeUInt ( 16 , X ) => #range ( minUInt16 <= X <= maxUInt16 ) [macro]
rule #rangeUInt ( 48 , X ) => #range ( minUInt48 <= X <= maxUInt48 ) [macro]
rule #rangeUInt ( 128 , X ) => #range ( minUInt128 <= X <= maxUInt128 ) [macro]
+ rule #rangeUInt ( 160 , X ) => #range ( minUInt160 <= X <= maxUInt160 ) [macro]
rule #rangeUInt ( 256 , X ) => #range ( minUInt256 <= X <= maxUInt256 ) [macro]
rule #rangeSFixed ( 128 , 10 , X ) => #range ( minSFixed128x10 <= X <= maxSFixed128x10 ) [macro]
rule #rangeUFixed ( 128 , 10 , X ) => #range ( minUFixed128x10 <= X <= maxUFixed128x10 ) [macro]
@@ -411,22 +412,25 @@ A cons-list is used for the EVM wordstack.
- `WS [ N := W ]` sets element $N$ of $WS$ to $W$ (padding with zeros as needed).
```k
- syntax Int ::= WordStack "[" Int "]" [function]
- // -----------------------------------------------
+ syntax Int ::= WordStack "[" Int "]" [function, functional]
+ // -----------------------------------------------------------
rule (W : _):WordStack [ N ] => W requires N ==Int 0
rule WS:WordStack [ N ] => #drop(N, WS) [ 0 ] requires N >Int 0
+ rule WS:WordStack [ N ] => 0 requires N W : WS requires N ==Int 0
rule (W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0
+ rule WS:WordStack [ N := W ] => WS requires N (0 : .WordStack) [ N := W ]
```
-- Definedness conditions for `WS [ N ]` and `WS [ N := W ]`
+- Definedness conditions for `WS [ N ]`:
```{.k .symbolic}
- rule #Ceil(WS[N]) => {((0 <=Int N) andBool (N {((0 <=Int N) andBool (N VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere]
+ rule #Ceil(#lookup( .Map, _ )) => true [anywhere]
```
- `#sizeWordStack` calculates the size of a `WordStack`.
@@ -475,12 +479,13 @@ Most of EVM data is held in local memory.
```{.k .membytes}
syntax Memory = Bytes
- syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)]
- // -------------------------------------------------------------------------------------
- rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete]
+ syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, functional, klabel(mapWriteBytes)]
+ // -------------------------------------------------------------------------------------------------
+ rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') requires START >=Int 0 [concrete]
+ rule WS [ START := WS':ByteArray ] => .Memory requires START LM [ START .. WIDTH ] [concrete]
syntax Memory ::= ".Memory" [function]
@@ -564,41 +569,45 @@ The local memory of execution is a byte-array (instead of a word-array).
// --------------------------------------------------------
rule .ByteArray => .Bytes [macro]
- syntax Int ::= #asWord ( ByteArray ) [function, smtlib(asWord)]
- // ---------------------------------------------------------------
- rule #asWord(WS) => chop(Bytes2Int(WS, BE, Unsigned))
+ syntax Int ::= #asWord ( ByteArray ) [function, functional, smtlib(asWord)]
+ // ---------------------------------------------------------------------------
+ rule #asWord(WS) => chop(Bytes2Int(WS, BE, Unsigned)) [concrete]
- syntax Int ::= #asInteger ( ByteArray ) [function]
- // --------------------------------------------------
- rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned)
+ syntax Int ::= #asInteger ( ByteArray ) [function, functional]
+ // --------------------------------------------------------------
+ rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete]
syntax Account ::= #asAccount ( ByteArray ) [function]
// ------------------------------------------------------
rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0
rule #asAccount(BS) => #asWord(BS) [owise]
- syntax ByteArray ::= #asByteStack ( Int ) [function]
- // ----------------------------------------------------
- rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned)
+ syntax ByteArray ::= #asByteStack ( Int ) [function, functional]
+ // ----------------------------------------------------------------
+ rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete]
- syntax ByteArray ::= ByteArray "++" ByteArray [function, right, klabel(_++_WS), smtlib(_plusWS_)]
- // -------------------------------------------------------------------------------------------------
- rule WS ++ WS' => WS +Bytes WS'
+ syntax ByteArray ::= ByteArray "++" ByteArray [function, functional, right, klabel(_++_WS), smtlib(_plusWS_)]
+ // -------------------------------------------------------------------------------------------------------------
+ rule WS ++ WS' => WS +Bytes WS' [concrete]
- syntax ByteArray ::= ByteArray "[" Int ".." Int "]" [function]
- // --------------------------------------------------------------
- rule WS [ START .. WIDTH ] => substrBytes(padRightBytes(WS, START +Int WIDTH, 0), START, START +Int WIDTH) requires START padRightBytes(.Bytes, WIDTH, 0) [owise]
+ syntax ByteArray ::= ByteArray "[" Int ".." Int "]" [function, functional]
+ // --------------------------------------------------------------------------
+ rule WS [ START .. WIDTH ] => padRightBytes(.Bytes, WIDTH, 0) [concrete, owise]
+ rule WS [ START .. WIDTH ] => .ByteArray requires notBool (WIDTH >=Int 0 andBool START >=Int 0)
+ rule WS [ START .. WIDTH ] => substrBytes(padRightBytes(WS, START +Int WIDTH, 0), START, START +Int WIDTH)
+ requires WIDTH >=Int 0 andBool START >=Int 0 andBool START lengthBytes(WS) [concrete]
- syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function]
- | #padRightToWidth ( Int , ByteArray ) [function]
- // --------------------------------------------------------------------
- rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0)
- rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0)
+ syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function, functional]
+ | #padRightToWidth ( Int , ByteArray ) [function, functional]
+ // --------------------------------------------------------------------------------
+ rule #padToWidth(N, BS) => BS requires notBool (N >=Int 0)
+ rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires N >=Int 0 [concrete]
+ rule #padRightToWidth(N, BS) => BS requires notBool (N >=Int 0)
+ rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires N >=Int 0 [concrete]
```
```{.k .nobytes}
@@ -640,8 +649,8 @@ The local memory of execution is a byte-array (instead of a word-array).
// --------------------------------------------------------------------------------
rule WS [ START .. WIDTH ] => #take(WIDTH, #drop(START, WS))
- syntax Int ::= #sizeByteArray ( ByteArray ) [function, functional, memo]
- // ------------------------------------------------------------------------
+ syntax Int ::= #sizeByteArray ( ByteArray ) [function, functional, smtlib(sizeByteArray), memo]
+ // -----------------------------------------------------------------------------------------------
rule #sizeByteArray ( WS ) => #sizeWordStack(WS) [concrete]
syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function, functional, memo]
@@ -681,8 +690,8 @@ Addresses
```k
syntax Int ::= #lookup ( Map , Int ) [function]
// -----------------------------------------------
- rule [#lookup.some]: #lookup( (KEY |-> VAL) M, KEY ) => VAL
- rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
+ rule [#lookup.some]: #lookup( (KEY |-> VAL:Int) M, KEY ) => VAL
+ rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
```
### Substate Log
diff --git a/evm.md b/evm.md
index 5d10604941..1d4c55140d 100644
--- a/evm.md
+++ b/evm.md
@@ -46,6 +46,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
// H_RETURN
.StatusCode
+ 0
.List
.List
.Set
@@ -256,12 +257,15 @@ Control Flow
- `#halt` indicates end of execution.
It will consume anything related to the current computation behind it on the `` cell.
-- `#end_` sets the `statusCode` then halts execution.
+- `#end_` sets the `statusCode` and the program counter of the last executed opcode, then halts execution.
```k
syntax KItem ::= "#halt" | "#end" StatusCode
// --------------------------------------------
- rule #end SC => #halt ... _ => SC
+ rule #end SC => #halt ...
+ _ => SC
+ _ => PCOUNT
+ PCOUNT
rule #halt ~> (_:Int => .) ...
rule #halt ~> (_:OpCode => .) ...
@@ -297,7 +301,7 @@ If the program-counter points to an actual opcode, it's loaded into the `#next [
The `#next [_]` operator initiates execution by:
1. checking if there will be a stack over/underflow, or a static mode violation,
-2. loading any additional state needed (when executing in full-node mode),
+2. calculate any address conversions needed for items on the wordstack,
3. executing the opcode (which includes any gas deduction needed), and
4. adjusting the program counter.
@@ -305,7 +309,7 @@ The `#next [_]` operator initiates execution by:
syntax InternalOp ::= "#next" "[" OpCode "]"
// --------------------------------------------
rule #next [ OP ]
- => #load [ OP ]
+ => #addr [ OP ]
~> #exec [ OP ]
~> #pc [ OP ]
...
@@ -420,7 +424,6 @@ The `#next [_]` operator initiates execution by:
```
Here we load the correct number of arguments from the `wordStack` based on the sort of the opcode.
-Some of them require an argument to be interpereted as an address (modulo 160 bits), so the `#addr?` function performs that check.
```k
syntax KItem ::= OpCode
@@ -457,61 +460,35 @@ The `CallOp` opcodes all interperet their second argument as an address.
rule #exec [ CO:CallOp ] => #gas [ CO , CO W0 W1 W2 W3 W4 W5 W6 ] ~> CO W0 W1 W2 W3 W4 W5 W6 ... W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS
```
-### Helpers
+### Address Conversion
-- `#addr` decides if the given argument should be interpreted as an address (given the opcode).
+Some opcodes require accessing elements of the state at different addresses.
+We make sure the given arguments (to be interpreted as addresses) are with 160 bits ahead of time.
```k
- syntax InternalOp ::= "#load" "[" OpCode "]"
+ syntax InternalOp ::= "#addr" "[" OpCode "]"
// --------------------------------------------
- rule #load [ OP:OpCode ] => #loadAccount #addr(W0) ...
+ rule #addr [ OP:OpCode ] => . ...
(W0 => #addr(W0)) : WS
- requires #addr?(OP)
+ requires OP ==K BALANCE
+ orBool OP ==K SELFDESTRUCT
+ orBool OP ==K EXTCODEHASH
+ orBool OP ==K EXTCODESIZE
+ orBool OP ==K EXTCODECOPY
- rule #load [ OP:OpCode ] => #loadAccount #addr(W0) ~> #lookupCode #addr(W0) ...
- (W0 => #addr(W0)) : WS
- requires #code?(OP)
-
- rule #load [ OP:OpCode ] => #loadAccount #addr(W1) ~> #lookupCode #addr(W1) ...
+ rule #addr [ OP:OpCode ] => . ...
W0 : (W1 => #addr(W1)) : WS
requires isCallOp(OP) orBool isCallSixOp(OP)
- rule #load [ CREATE ] => #loadAccount #newAddr(ACCT, NONCE) ...
- ACCT
-
- ACCT
- NONCE
- ...
-
-
- rule #load [ OP:OpCode ] => #lookupStorage ACCT W0 ...
- ACCT
- W0 : WS
- requires OP ==K SSTORE orBool OP ==K SLOAD
-
- rule #load [ OP:OpCode ] => . ...
- requires notBool (
- OP ==K CREATE orBool
- OP ==K SLOAD orBool
- OP ==K SSTORE orBool
- isCallOp (OP) orBool
- isCallSixOp(OP) orBool
- #addr?(OP) orBool
- #code?(OP)
- )
-
- syntax Bool ::= "#addr?" "(" OpCode ")" [function]
- // --------------------------------------------------
- rule #addr?(BALANCE) => true
- rule #addr?(SELFDESTRUCT) => true
- rule #addr?(EXTCODEHASH) => true
- rule #addr?(OP) => false requires (OP =/=K BALANCE) andBool (OP =/=K SELFDESTRUCT) andBool (OP =/=K EXTCODEHASH)
-
- syntax Bool ::= "#code?" "(" OpCode ")" [function]
- // --------------------------------------------------
- rule #code?(EXTCODESIZE) => true
- rule #code?(EXTCODECOPY) => true
- rule #code?(OP) => false requires (OP =/=K EXTCODESIZE) andBool (OP =/=K EXTCODECOPY)
+ rule #addr [ OP:OpCode ] => . ...
+ requires notBool ( OP ==K BALANCE
+ orBool OP ==K SELFDESTRUCT
+ orBool OP ==K EXTCODEHASH
+ orBool OP ==K EXTCODESIZE
+ orBool OP ==K EXTCODECOPY
+ orBool isCallOp(OP)
+ orBool isCallSixOp(OP)
+ )
```
### Program Counter
@@ -644,7 +621,7 @@ After executing a transaction, it's necessary to have the effect of the substate
- `#finalizeBlock` is used to signal that block finalization procedures should take place (after transactions have executed).
- `#rewardOmmers(_)` pays out the reward to uncle blocks so that blocks are orphaned less often in Ethereum.
-```{.k .standalone}
+```k
syntax EthereumCommand ::= "#startBlock"
// ----------------------------------------
rule #startBlock => . ...
@@ -790,40 +767,6 @@ These are just used by the other operators for shuffling local execution state a
```
-The following operations help with loading account information from an external running client.
-This minimizes the amount of information which must be stored in the configuration.
-
-- `#loadAccount` queries for account data from the running client.
-- `#lookupCode` loads the code of an account into the `` cell.
-- `#lookupStorage` loads the value of the specified storage key into the `` cell.
-
-```k
- syntax InternalOp ::= "#loadAccount" Int
- | "#lookupCode" Int
- | "#lookupStorage" Int Int
- // ----------------------------------------------
-```
-
-In `standalone` mode, the semantics assumes that all relevant account data is already loaded into memory.
-
-```{.k .standalone}
- rule #loadAccount _ => . ...
- rule #lookupCode _ => . ...
- rule #lookupStorage _ _ => . ...
-```
-
-In `node` mode, the semantics are given in terms of an external call to a running client.
-
-```{.k .node}
- rule #lookupStorage ACCT INDEX => . ...
-
- ACCT
- STORAGE:Map
- ...
-
- requires INDEX in_keys(STORAGE)
-```
-
- `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist.
```k
@@ -1041,7 +984,7 @@ These operators make queries about the current execution state.
When running as a `node`, the blockhash will be retrieved from the running client.
Otherwise, it is calculated here using the "shortcut" formula used for running tests.
-```{.k .standalone}
+```k
rule BLOCKHASH N => #blockhash(HASHES, N, HI -Int 1, 0) ~> #push ...
HI
HASHES
@@ -1386,7 +1329,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
_ => .WordStack
_ => .Memory
- syntax Set ::= #computeValidJumpDests(ByteArray) [function]
+ syntax Set ::= #computeValidJumpDests(ByteArray) [function, memo]
| #computeValidJumpDests(ByteArray, Int, List) [function, klabel(#computeValidJumpDestsAux)]
// ---------------------------------------------------------------------------------------------------------
rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, .List)
@@ -1632,15 +1575,12 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
```
`CREATE2` will attempt to `#create` the account, but with the new scheme for choosing the account address.
-Note that we cannot execute #loadAccount during the #load phase earlier because gas will not yet
-have been paid, and it may be to expensive to compute the hash of the init code.
```k
syntax QuadStackOp ::= "CREATE2"
// --------------------------------
rule CREATE2 VALUE MEMSTART MEMWIDTH SALT
- => #loadAccount #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
- ~> #checkCall ACCT VALUE
+ => #checkCall ACCT VALUE
~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH)
~> #codeDeposit #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
...
@@ -2556,8 +2496,8 @@ After interpreting the strings representing programs as a `WordStack`, it should
- `#dasmOpCode` interperets a `Int` as an `OpCode`.
```k
- syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function]
- // -----------------------------------------------------------
+ syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function, memo]
+ // -----------------------------------------------------------------
rule #dasmOpCode( 0, _ ) => STOP
rule #dasmOpCode( 1, _ ) => ADD
rule #dasmOpCode( 2, _ ) => MUL
diff --git a/json.md b/json.md
index ef4c1b5fcf..907ea4cfe5 100644
--- a/json.md
+++ b/json.md
@@ -1,7 +1,11 @@
-### JSON Formatting
+KJSON
+=====
-The JSON format is used extensively for communication in the Ethereum circles.
-Writing a JSON-ish parser in K takes 6 lines.
+This is a non-faithful implementation of the [ECMA-404 JSON Data Interchange Format](http://www.ecma-international.org/publications/files/ECMA-ST/ECMA-404.pdf).
+There are issues with how `JSONNumber` and `JSONString` are specified here, because we use K's `String` and `Int` sort directly, which are not quite correct.
+
+JSON Syntax
+-----------
```k
module JSON
@@ -12,19 +16,79 @@ module JSON
syntax JSONs ::= List{JSON,","} [klabel(JSONs) , symbol]
syntax JSONKey ::= String
syntax JSON ::= "null" [klabel(JSONnull) , symbol]
- | String | Int | Bool
+ | JSONKey | Bool
| JSONKey ":" JSON [klabel(JSONEntry) , symbol]
| "{" JSONs "}" [klabel(JSONObject) , symbol]
| "[" JSONs "]" [klabel(JSONList) , symbol]
// --------------------------------------------------------------------
```
+```k
+endmodule
+```
+
+JSON Extensions
+---------------
+
+Some common functions and extensions of JSON are provided here.
+
+```k
+module JSON-EXT
+ imports JSON
+```
+
+- `+JSONs` appends two JSON lists.
+- `reverseJSONs` reverses a JSON list.
+
+```k
+ syntax JSONs ::= JSONs "+JSONs" JSONs [function]
+ // ------------------------------------------------
+ rule .JSONs +JSONs JS' => JS'
+ rule (J , JS) +JSONs JS' => J , (JS +JSONs JS')
+
+ syntax JSONs ::= reverseJSONs ( JSONs ) [function]
+ | reverseJSONsAux ( JSONs , JSONs ) [function]
+ // -------------------------------------------------------------
+ rule reverseJSONs(JS) => reverseJSONsAux(JS, .JSONs)
+
+ rule reverseJSONsAux(.JSONs, JS') => JS'
+ rule reverseJSONsAux((J, JS:JSONs), JS') => reverseJSONsAux(JS, (J, JS'))
+```
+
+- `qsortJSONs` quick-sorts a list of key-value pairs.
+- `sortedJSONs` is a predicate saying whether a given list of JSONs is sorted or not.
+
+```k
+ syntax JSONs ::= qsortJSONs ( JSONs ) [function]
+ | #entriesLT ( String , JSONs ) [function]
+ | #entriesGE ( String , JSONs ) [function]
+ // ---------------------------------------------------------
+ rule qsortJSONs(.JSONs) => .JSONs
+ rule qsortJSONs(KEY : VALUE, REST) => qsortJSONs(#entriesLT(KEY, REST)) +JSONs (KEY : VALUE , qsortJSONs(#entriesGE(KEY, REST)))
+
+ rule #entriesLT(KEY, .JSONs) => .JSONs
+ rule #entriesLT(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesLT(KEY, REST) requires KEY' #entriesLT(KEY, REST) requires notBool KEY' .JSONs
+ rule #entriesGE(KEY, (KEY': VALUE, REST)) => KEY': VALUE , #entriesGE(KEY, REST) requires KEY' >=String KEY
+ rule #entriesGE(KEY, (KEY': VALUE, REST)) => #entriesGE(KEY, REST) requires notBool KEY' >=String KEY
+
+ syntax Bool ::= sortedJSONs ( JSONs ) [function]
+ // ------------------------------------------------
+ rule sortedJSONs( .JSONs ) => true
+ rule sortedJSONs( KEY : _ ) => true
+ rule sortedJSONs( (KEY : _) , (KEY' : VAL) , REST ) => KEY <=String KEY' andThenBool sortedJSONs((KEY' : VAL) , REST)
+```
+
**TODO**: Adding `Int` to `JSONKey` is a hack to make certain parts of semantics easier.
```k
syntax JSONKey ::= Int
// ----------------------
+```
+```k
endmodule
```
@@ -35,12 +99,12 @@ JSON-RPC
module JSON-RPC
imports K-IO
imports LIST
- imports JSON
+ imports JSON-EXT
configuration
- $SOCK:Int
- 0:IOInt
+ $INPUT:Int
+ $OUTPUT:Int
"":JSON
0:JSON
diff --git a/kevm b/kevm
index 613f904579..aea94e9061 100755
--- a/kevm
+++ b/kevm
@@ -3,13 +3,23 @@
set -euo pipefail
shopt -s extglob
+notif() { echo "== $@" >&2 ; }
+fatal() { echo "[FATAL] $@" ; exit 1 ; }
+
kevm_dir="${KEVM_DIR:-.}"
build_dir="$kevm_dir/.build"
defn_dir="${KEVM_DEFN_DIR:-$build_dir/defn}"
lib_dir="$build_dir/local/lib"
k_release_dir="${K_RELEASE:-$kevm_dir/deps/k/k-distribution/target/release/k}"
+if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then
+ if which kompile &> /dev/null; then
+ k_release_dir="$(dirname $(which kompile))/.."
+ else
+ fatal "Cannot find K Installation!"
+ fi
+fi
-export PATH="$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH"
+export PATH="${defn_dir}/web3/build:$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH"
export LD_LIBRARY_PATH="$k_release_dir/lib/native/linux64:$lib_dir:${LD_LIBRARY_PATH:-}"
test_logs="$build_dir/logs"
@@ -20,28 +30,6 @@ KLAB_OUT="${KLAB_OUT:-$build_dir/klab}"
KLAB_NODE_STACK_SIZE="${KLAB_NODE_STACK_SIZE:-30000}"
export KLAB_OUT
-# Utilities
-# ---------
-
-notif() { echo "== $@" >&2 ; }
-fatal() { echo "[FATAL] $@" ; exit 1 ; }
-
-pretty_diff() {
- git --no-pager diff --no-index --ignore-all-space "$@"
-}
-
-get_port() {
- python3 -c """
-import socket
-
-s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
-s.bind(('', 0))
-addr = s.getsockname()
-print(str(addr[1]))
-s.close()
-"""
-}
-
# Runners
# -------
@@ -97,27 +85,22 @@ run_search() {
}
run_web3() {
- local web3_port
- web3_port="$1" ; shift
- kevm_port=$(get_port)
run_file='-'
if $debug; then
- gdb --args ${defn_dir}/web3/build/kevm-client --port "$web3_port" --kport "$kevm_port" "$@"
+ gdb --args kevm-client --port "$kevm_port" --host "$kevm_host" "$@"
elif $dump; then
- exec -a "$0 web3" ${defn_dir}/web3/build/kevm-client --dump --port "$web3_port" --kport "$kevm_port" "$@" 3>&2 2>&1 1>&3 \
+ exec -a "$0 web3" kevm-client --dump --port "$kevm_port" --host "$kevm_host" "$@" 3>&2 2>&1 1>&3 \
| "$0" kast --backend web3 - pretty --input kore --sort GeneratedTopCell
else
- exec -a "$0 web3" ${defn_dir}/web3/build/kevm-client --port "$web3_port" --kport "$kevm_port" "$@" 2>/dev/null
+ exec -a "$0 web3" kevm-client --port "$kevm_port" --host "$kevm_host" "$@" 2>/dev/null
fi
}
run_web3_send() {
- local web3_port web3_method web3_params web3_file
- web3_port="$1" ; shift
-
+ local web3_method web3_params web3_file
if [[ -f "$1" ]]; then
web3_file="$1" ; shift
- curl -s -X POST 127.0.0.1:$web3_port --data @$web3_file
+ curl -s -X POST $kevm_host:$kevm_port --data @$web3_file
else
web3_method="$1" ; shift
join_args() {
@@ -125,32 +108,10 @@ run_web3_send() {
echo "$*"
}
web3_params="$(join_args "$@")"
- curl -s -X POST --data '{"jsonrpc": "2.0", "id": 1, "method": "'"$web3_method"'", "params": ['"$web3_params"']}' 127.0.0.1:"$web3_port"
+ curl -s -X POST --data '{"jsonrpc": "2.0", "id": 1, "method": "'"$web3_method"'", "params": ['"$web3_params"']}' "$kevm_host":"$kevm_port"
fi
}
-run_web3_ganache() {
- local web3_port
- web3_port="$1" ; shift
-
- notif 'Launching web3 client'
- $0 web3 "${args[@]}" "$web3_port" "$@" &
- while ! netcat -z 127.0.0.1 "$web3_port" ; do sleep 0.1; done
- notif 'Generating accounts'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xdc7e9a7c64933ab893160b79d099c254d274e1c40c6df6d5239e1a623e3d6de1", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x6e2687f9732d970c6b1d5baa3dff26c4af36257552bc17df737afbc00ca70de2", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xd34d8e873da77217abaef9424a7d87fce351b603920c7f5288d7701c5f148860", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x976b5ec9253759d4a2746c37597841beba57527123dc3db2165b637adce58bcb", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x23dff7ac7981167eb5386e51c3d6d2e3ca9dc219315749b2058d0a2d1e21625e", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xe040e4bf96d8c9d3a8d1ffb22b30ed4b0a79a25342d656c5a8e2784b0fab752f", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x13abddd7d94165fc46bed2cad6b0b14cd0267a85f70ad5c26cce82c609e0bf87", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x0e29f7d6984bb47d60db479212ca56af516705b07d8753b474bd7f0db8bc1921", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xea7fe1480e9ab71c261c5e1e727f36482f84dbdb07dbf8c8e9f767dcecf87568", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x5f9addbbf41ae2e3d6cb7b07ffabf2c5ff6edc3a38c9dd64a9afd23df02ad7ee", "balance":"0x56BC75E2D63100000"}'
- $0 web3-send "$web3_port" firefly_genesisBlock
-
-}
-
run_klab() {
local run_mode klab_log def_module
@@ -240,9 +201,8 @@ if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
$0 kast [--backend (llvm|java|haskell|web3)]
- PCOUNT
+ PCOUNT
RD
TXID
@@ -1497,7 +1558,7 @@ NOGAS Mode
NOGAS
[priority(25)]
- rule #validateTx TXID => #executeTx TXID ~> #makeTxReceipt TXID ~> #finishTx ...
+ rule #validateTx TXID => #updateTimestamp ~> #executeTx TXID ~> #mineAndUpdate ...
NOGAS
[priority(25)]
@@ -1670,7 +1731,7 @@ Timestamp Calls
// -----------------------------------
rule #firefly_setTime => #rpcResponseSuccess(true) ...
[ TIME:String, .JSONs ]
- _ => #parseHexWord( TIME )
+ _ => #parseHexWord( TIME ) -Int #time()
rule #firefly_setTime => #rpcResponseSuccess(false) ... [owise]
```
@@ -1681,28 +1742,62 @@ Gas Limit Call
```k
syntax KItem ::= "#firefly_setGasLimit"
// ---------------------------------------
- rule #firefly_setGasLimit => #rpcResponseSuccess(true) ...
- [ GLIMIT:String, .JSONs ]
- _ => #parseWord( GLIMIT )
+ rule #firefly_setGasLimit ...
+ [ GLIMIT:String => #parseWord( GLIMIT ), .JSONs ]
rule #firefly_setGasLimit => #rpcResponseSuccess(true) ...
- [ GLIMIT:Int, .JSONs ]
- _ => GLIMIT
+ [ GLIMIT:Int, .JSONs ]
+ _ => GLIMIT
+ _ => GLIMIT
rule #firefly_setGasLimit => #rpcResponseError(-32000, "firefly_setGasLimit requires exactly 1 argument") ... [owise]
```
+Gas Price Call
+--------------
+
+```k
+ syntax KItem ::= "#firefly_setGasPrice"
+ // ---------------------------------------
+ rule #firefly_setGasPrice ...
+ [ GPRICE:String => #parseWord( GPRICE ), .JSONs ]
+
+ rule #firefly_setGasPrice => #rpcResponseSuccess(true) ...
+ [ GPRICE:Int, .JSONs ]
+ _ => GPRICE
+ _ => GPRICE
+
+ rule #firefly_setGasPrice => #rpcResponseError(-32000, "firefly_setGasPrice requires exactly 1 argument") ... [owise]
+```
+
+Network Id
+----------
+
+```k
+ syntax KItem ::= "#firefly_setNetworkId"
+ // ----------------------------------------
+ rule #firefly_setNetworkId ...
+ [ VALUE:String => #parseWord( VALUE ), .JSONs ]
+
+ rule #firefly_setNetworkId => #rpcResponseSuccess(true) ...
+ [ VALUE:Int, .JSONs ]
+ _ => VALUE
+
+ rule #firefly_setNetworkId => #rpcResponseError(-32000, "firefly_setNetworkId requires exactly 1 argument") ... [owise]
+```
+
Mining
------
```k
syntax KItem ::= "#evm_mine"
// ----------------------------
- rule #evm_mine => #mineBlock ~> #rpcResponseSuccess("0x0") ... [owise]
+ rule #evm_mine => #updateTimestamp ~> #mineBlock ~> #rpcResponseSuccess("0x0") ... [owise]
rule #evm_mine => #mineBlock ~> #rpcResponseSuccess("0x0") ...
- [ TIME:String, .JSONs ]
- _ => #parseWord( TIME )
+ [ TIME:String, .JSONs ]
+ _ => #parseWord( TIME )
+ _ => #parseWord( TIME ) -Int #time()
rule #evm_mine => #rpcResponseError(-32000, "Incorrect number of arguments. Method 'evm_mine' requires between 0 and 1 arguments.") ...
[ _ , _ , _:JSONs ]
@@ -1712,17 +1807,19 @@ Mining
rule #firefly_genesisBlock ...
[ .JSONs => #unparseQuantity(#time()), .JSONs ]
- rule #firefly_genesisBlock => #updateTrieRoots ~> #pushBlockchainState ~> #rpcResponseSuccess(true) ...
+ rule #firefly_genesisBlock => #updateTrieRoots ~> #pushBlockchainState ~> #incrementBlockNumber ~> #rpcResponseSuccess(true) ...
[ TIME:String, .JSONs ]
_ => #parseWord( TIME )
_ => #padToWidth( 256, .ByteArray )
_ => 13478047122767188135818125966132228187941283477090363246179690878162135454535
+ _ => #parseWord( TIME ) -Int #time()
syntax KItem ::= "#mineBlock"
// -----------------------------
rule #mineBlock
=> #finalizeBlock
~> #setParentHash #getBlockByNumber( LATEST, BLOCKLIST, { NETWORK | BLOCK } )
+ ~> #makeTxReceipts
~> #updateTrieRoots
~> #saveState
~> #startBlock
@@ -1744,7 +1841,7 @@ Mining
| "#updateTransactionsRoot"
| "#updateReceiptsRoot"
// --------------------------------------
- rule #saveState => #incrementBlockNumber ~> #pushBlockchainState ...
+ rule #saveState => #pushBlockchainState ~> #incrementBlockNumber ...
rule #incrementBlockNumber => . ...
BN => BN +Int 1
@@ -1777,7 +1874,8 @@ Mining
syntax KItem ::= "#updateTimestamp"
// -----------------------------------
rule #updateTimestamp => . ...
- PREV => #if PREV <=Int #time() #then #time() #else PREV #fi
+ _ => #time() +Int TIMEDIFF
+ TIMEDIFF
```
Retrieving logs
@@ -1806,7 +1904,7 @@ Retrieving logs
[ { PARAMS => "toBlock": "latest", PARAMS } , .JSONs ]
requires #getJSON("toBlock", { PARAMS }) ==K undef
- rule #eth_getLogs => #getLogs(#parseBlockIdentifier(#getString("fromBlock", { PARAMS })), #parseBlockIdentifier(#getString("toBlock", { PARAMS })), .List) ...
+ rule #eth_getLogs => #getLogs(#parseBlockIdentifier(#getJSON("fromBlock", { PARAMS })), #parseBlockIdentifier(#getJSON("toBlock", { PARAMS })), .List) ...
[ { PARAMS } , .JSONs ]
requires #getJSON("fromBlock", { PARAMS }) =/=K undef
andBool #getJSON("toBlock" , { PARAMS }) =/=K undef
@@ -1896,7 +1994,6 @@ Unimplemented Methods
| "#eth_syncing"
| "#bzz_hive"
| "#bzz_info"
- | "#debug_traceTransaction"
| "#miner_start"
| "#miner_stop"
| "#personal_sendTransaction"
@@ -1927,7 +2024,6 @@ Unimplemented Methods
rule #eth_syncing => #rpcResponseUnimplemented ...
rule #bzz_hive => #rpcResponseUnimplemented ...
rule #bzz_info => #rpcResponseUnimplemented ...
- rule #debug_traceTransaction => #rpcResponseUnimplemented ...
rule #miner_start => #rpcResponseUnimplemented ...
rule #miner_stop => #rpcResponseUnimplemented ...
rule #personal_sendTransaction => #rpcResponseUnimplemented ...