Organize repository, move sources into subdirectories (#1433)

* *.md => include/*.md: move k sources into src directory

* Makefile: do not include test-suite specific lemma suites in package

* Makefile, include/{. => kframework}/*.md: add subdirectory

* Makefile, {tests/specs/ => include/kframework/lemmas}: move lemmas into include directory

* Makefile: use relative path for PLUGIN_SUBMODULE

* Makefile: include plugin in kframework directory directly

* Makefile, cmake/: adjust for new directory structure of K imports

* include/serialization: adjust import of krypto

* tests/specs: adjust lemmas include

* Makefile, kevm: remove now uneeded -I option for plugin

* Makefile, kevm => bin/kevm: move script into subdirectory

* flake.nix: adjust path for kevm

* tests/erc20/verification: correct lemmas import

* include/{buf, abi}: move definition of ceil32

* include/lemmas: lower dependency from EDSL => BUF for LEMMAS module

* tests/lemmas-spec: adjust lemmas-spec to include EDSL

* Makefile: correct path of optimizations module

* Makefile: correct Foundry build

* .github/test-pr: build foundry definition ahead of time

* tests/specs/opcodes: adjust requires

* tests/specs/benchmarks: adjust requires

* tests/specs/benchmarks/verification: correct module import

* package/nix/kevm.patch: correct patch

* tests/specs/benchmarks: add lemma module back in for verification

* tests/specs/benchmarks: simplify imports

* tests/specs/functional/lemmas-spec: adjust imports

Author: ehildenb

.github/workflows/test-pr.yml

@@ -106,6 +106,8 @@ jobs:
           tag: kevm-ci-foundry-${{ github.sha }}
       - name: 'Build kevm-pyk'
         run: docker exec -t kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make kevm-pyk venv -j2'
+      - name: 'Build Foundry'
+        run: docker exec -t kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
       - name: 'Test Foundry'
         run: docker exec -t kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=4'
       - name: 'Tear down Docker'

Makefile

@@ -40,9 +40,10 @@ export C_INCLUDE_PATH
 export CPLUS_INCLUDE_PATH
 export PATH
 
-PLUGIN_SUBMODULE := $(abspath $(DEPS_DIR)/plugin)
+PLUGIN_SUBMODULE := $(DEPS_DIR)/plugin
 PLUGIN_SOURCE    := $(KEVM_INCLUDE)/kframework/blockchain-k-plugin/krypto.md
-export PLUGIN_SUBMODULE
+PLUGIN_FULL_PATH := $(abspath ${PLUGIN_SUBMODULE})
+export PLUGIN_FULL_PATH
 
 
 .PHONY: all clean distclean                                                                                                      \
@@ -147,17 +148,18 @@ k-deps:
 	    && mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(INSTALL_LIB)/kframework -Dllvm.backend.destdir=$(CURDIR)/$(BUILD_DIR) -Dproject.build.type=$(K_BUILD_TYPE) $(K_MVN_ARGS) \
 	    && DESTDIR=$(CURDIR)/$(BUILD_DIR) PREFIX=$(INSTALL_LIB)/kframework package/package
 
+plugin_k_include  := $(KEVM_INCLUDE)/kframework/plugin
 plugin_include    := $(KEVM_LIB)/blockchain-k-plugin/include
 plugin_k          := krypto.md
 plugin_c          := plugin_util.cpp crypto.cpp blake2.cpp plugin_util.h blake2.h
-plugin_includes   := $(patsubst %, $(plugin_include)/kframework/%, $(plugin_k))
-plugin_c_includes := $(patsubst %, $(plugin_include)/c/%,          $(plugin_c))
+plugin_includes   := $(patsubst %, $(plugin_k_include)/%, $(plugin_k))
+plugin_c_includes := $(patsubst %, $(plugin_include)/c/%, $(plugin_c))
 
 $(plugin_include)/c/%: $(PLUGIN_SUBMODULE)/plugin-c/%
 	@mkdir -p $(dir $@)
 	install $< $@
 
-$(plugin_include)/kframework/%: $(PLUGIN_SUBMODULE)/plugin/%
+$(plugin_k_include)/%: $(PLUGIN_SUBMODULE)/plugin/%
 	@mkdir -p $(dir $@)
 	install $< $@
 
@@ -168,48 +170,40 @@ plugin-deps: $(plugin_includes) $(plugin_c_includes)
 
 KOMPILE := $(KEVM) kompile
 
-kevm_files := abi.md              \
-              asm.md              \
-              buf.md              \
-              data.md             \
-              driver.md           \
-              edsl.md             \
-              evm.md              \
-              evm-types.md        \
-              evm-node.md         \
-              foundry.md          \
-              hashed-locations.md \
-              infinite-gas.md     \
-              json-rpc.md         \
-              network.md          \
-              optimizations.md    \
-              serialization.md    \
-              state-utils.md      \
-              word.md
-
-kevm_lemmas := lemmas.k             \
-               int-simplification.k \
-               erc20/evm-symbolic.k \
-               mcd/bin_runtime.k    \
-               mcd/storage.k        \
-               mcd/verification.k   \
-               mcd/word-pack.k
-
-lemma_includes := $(patsubst %, $(KEVM_INCLUDE)/kframework/lemmas/%, $(kevm_lemmas))
+kevm_files := abi.md                      \
+              asm.md                      \
+              buf.md                      \
+              data.md                     \
+              driver.md                   \
+              edsl.md                     \
+              evm.md                      \
+              evm-types.md                \
+              evm-node.md                 \
+              foundry.md                  \
+              hashed-locations.md         \
+              infinite-gas.md             \
+              json-rpc.md                 \
+              network.md                  \
+              optimizations.md            \
+              serialization.md            \
+              state-utils.md              \
+              word.md                     \
+              lemmas/lemmas.k             \
+              lemmas/int-simplification.k
 
 kevm_includes := $(patsubst %, $(KEVM_INCLUDE)/kframework/%, $(kevm_files))
 
-includes := $(kevm_includes) $(lemma_includes) $(plugin_includes) $(plugin_c_includes)
+includes := $(kevm_includes) $(plugin_includes) $(plugin_c_includes)
 
-$(KEVM_INCLUDE)/kframework/%.md: %.md
+$(KEVM_INCLUDE)/%: include/%
 	@mkdir -p $(dir $@)
 	install $< $@
 
 $(KEVM_INCLUDE)/kframework/lemmas/%.k: tests/specs/%.k
 	@mkdir -p $(dir $@)
 	install $< $@
 
-KOMPILE_OPTS = -I $(INSTALL_INCLUDE)/kframework -I $(INSTALL_LIB)/blockchain-k-plugin/include/kframework
+KOMPILE_OPTS = -I $(INSTALL_INCLUDE)/kframework
 
 ifneq (,$(RELEASE))
     KOMPILE_OPTS += -O2
@@ -230,10 +224,11 @@ $(KEVM_LIB)/$(haskell_kompiled): $(libsecp256k1_out)
 endif
 
 $(KEVM_LIB)/$(haskell_kompiled): $(kevm_includes) $(plugin_includes) $(KEVM_BIN)/kevm
-	$(KOMPILE) --backend haskell                     \
-	    $(haskell_main_file) $(HASKELL_KOMPILE_OPTS) \
-	    --main-module $(haskell_main_module)         \
-	    --syntax-module $(haskell_syntax_module)     \
+	$(KOMPILE) --backend haskell                        \
+	    $(KEVM_INCLUDE)/kframework/$(haskell_main_file) \
+	    $(HASKELL_KOMPILE_OPTS)                         \
+	    --main-module $(haskell_main_module)            \
+	    --syntax-module $(haskell_syntax_module)        \
 	    $(KOMPILE_OPTS) $(KEVM_OPTS)
 
 # Standalone
@@ -250,10 +245,10 @@ $(KEVM_LIB)/$(llvm_kompiled): $(libcryptopp_out)
 endif
 
 $(KEVM_LIB)/$(llvm_kompiled): $(kevm_includes) $(plugin_includes) $(plugin_c_includes) $(libff_out) $(KEVM_BIN)/kevm
-	$(KOMPILE) --backend llvm                 \
-	    $(llvm_main_file)                     \
-	    --main-module $(llvm_main_module)     \
-	    --syntax-module $(llvm_syntax_module) \
+	$(KOMPILE) --backend llvm                        \
+	    $(KEVM_INCLUDE)/kframework/$(llvm_main_file) \
+	    --main-module $(llvm_main_module)            \
+	    --syntax-module $(llvm_syntax_module)        \
 	    $(KOMPILE_OPTS) $(KEVM_OPTS)
 
 # Node
@@ -268,10 +263,10 @@ node_kompiled      := $(node_dir)/build/kevm-vm
 export node_dir
 
 $(KEVM_LIB)/$(node_kore): $(kevm_includes) $(plugin_includes) $(plugin_c_includes) $(libff_out) $(KEVM_BIN)/kevm
-	$(KOMPILE) --backend node                 \
-	    $(node_main_file)                     \
-	    --main-module $(node_main_module)     \
-	    --syntax-module $(node_syntax_module) \
+	$(KOMPILE) --backend node                        \
+	    $(KEVM_INCLUDE)/kframework/$(node_main_file) \
+	    --main-module $(node_main_module)            \
+	    --syntax-module $(node_syntax_module)        \
 	    $(KOMPILE_OPTS) $(KEVM_OPTS)
 
 $(KEVM_LIB)/$(node_kompiled): $(KEVM_LIB)/$(node_kore) $(protobuf_out) $(libff_out)
@@ -293,10 +288,11 @@ $(KEVM_LIB)/$(foundry_kompiled): $(libsecp256k1_out)
 endif
 
 $(KEVM_LIB)/$(foundry_kompiled): $(kevm_includes) $(plugin_includes) $(lemma_includes) $(KEVM_BIN)/kevm
-	$(KOMPILE) --backend foundry                     \
-	    $(foundry_main_file) $(HASKELL_KOMPILE_OPTS) \
-	    --main-module $(foundry_main_module)         \
-	    --syntax-module $(foundry_syntax_module)     \
+	$(KOMPILE) --backend foundry                        \
+	    $(KEVM_INCLUDE)/kframework/$(foundry_main_file) \
+	    --main-module $(foundry_main_module)            \
+	    --syntax-module $(foundry_syntax_module)        \
+	    $(HASKELL_KOMPILE_OPTS)                         \
 	    $(KOMPILE_OPTS) $(KEVM_OPTS)
 
 # Installing
@@ -314,7 +310,7 @@ install_libs := $(haskell_kompiled)                                        \
                 release.md                                                 \
                 version
 
-$(KEVM_BIN)/kevm: kevm
+$(KEVM_BIN)/%: bin/%
 	@mkdir -p $(dir $@)
 	install $< $@
 
@@ -341,7 +337,7 @@ build: $(patsubst %, $(KEVM_BIN)/%, $(install_bins)) $(patsubst %, $(KEVM_LIB)/%
 build-llvm:     $(KEVM_LIB)/$(llvm_kompiled)    $(KEVM_LIB)/kore-json.py
 build-haskell:  $(KEVM_LIB)/$(haskell_kompiled) $(KEVM_LIB)/kore-json.py
 build-node:     $(KEVM_LIB)/$(node_kompiled)
-build-kevm:     $(KEVM_BIN)/kevm $(kevm_includes) $(lemma_includes) $(plugin_includes)
+build-kevm:     $(KEVM_BIN)/kevm $(kevm_includes) $(plugin_includes)
 build-foundry:  $(KEVM_LIB)/$(foundry_kompiled) $(KEVM_LIB)/kore-json.py
 
 all_bin_sources := $(shell find $(KEVM_BIN) -type f | sed 's|^$(KEVM_BIN)/||')
@@ -543,7 +539,7 @@ tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$
 	$(KEVM) prove $< $(KEVM_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) $(KPROVE_OPTS)                   \
 	    --definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
 
-tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT) tests/specs/concrete-rules.txt $(kevm_includes) $(lemma_includes) $(plugin_includes) $(KEVM_BIN)/kevm
+tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT) tests/specs/concrete-rules.txt $(kevm_includes) $(plugin_includes) $(KEVM_BIN)/kevm
 	$(KOMPILE) --backend $(word 3, $(subst /, , $*)) $<                                                  \
 	    --definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \
 	    --main-module $(KPROVE_MODULE)                                                                   \
@@ -664,7 +660,7 @@ test-klab-prove: KPROVE_OPTS += --debugger
 test-klab-prove: $(smoke_tests_prove:=.prove)
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
-tests/specs/opcodes/evm-optimizations-spec.md: optimizations.md
+tests/specs/opcodes/evm-optimizations-spec.md: include/kframework/optimizations.md
 	cat $< | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
 
 # Parse Tests

kevm renamed to bin/kevm

@@ -55,7 +55,7 @@ run_kevm_pyk() {
     case "${pyk_command}" in
         kompile|run|prove|solc-to-k|foundry-kompile|foundry-prove)
             pyk_args=(--definition "${backend_dir}")
-            pyk_args+=(-I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework")
+            pyk_args+=(-I "${INSTALL_INCLUDE}/kframework")
             ;;
     esac
     ! ${verbose} || pyk_args+=(--verbose)
@@ -73,7 +73,7 @@ run_kompile() {
 
     kompile_opts=( "${run_file}" --emit-json )
     ${pyk} || kompile_opts+=( --output-definition "${backend_dir}" )
-    ${pyk} || kompile_opts+=( -I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework" )
+    ${pyk} || kompile_opts+=( -I "${INSTALL_INCLUDE}/kframework" )
     ${pyk} || kompile_opts+=( --hook-namespaces "JSON KRYPTO BLOCKCHAIN" )
     ${pyk} || ! ${debug} || kompile_opts+=( --debug )
 
@@ -190,7 +190,7 @@ run_prove() {
     proof_args=("${run_file}")
     if ! ${pyk}; then
         proof_args+=(--definition "${backend_dir}")
-        proof_args+=( -I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework" )
+        proof_args+=( -I "${INSTALL_INCLUDE}/kframework" )
         ! ${debug} || proof_args+=(--debug)
     fi
 

cmake/node/CMakeLists.txt

@@ -50,9 +50,9 @@ add_executable(kevm-vm
 	$ENV{NODE_DIR}/vm/kevm/semantics.cpp
 	$ENV{NODE_DIR}/plugin-c/blockchain.cpp
 	$ENV{NODE_DIR}/plugin-c/world.cpp
-	$ENV{PLUGIN_SUBMODULE}/plugin-c/blake2.cpp
-	$ENV{PLUGIN_SUBMODULE}/plugin-c/crypto.cpp
-	$ENV{PLUGIN_SUBMODULE}/plugin-c/plugin_util.cpp
+	$ENV{PLUGIN_FULL_PATH}/plugin-c/blake2.cpp
+	$ENV{PLUGIN_FULL_PATH}/plugin-c/crypto.cpp
+	$ENV{PLUGIN_FULL_PATH}/plugin-c/plugin_util.cpp
 	$ENV{LOCAL_LIB}/proto/proto/msg.pb.cc)
 
 if(UNIX AND NOT APPLE)
@@ -65,7 +65,7 @@ if (APPLE)
 endif()
 
 target_include_directories(kevm-vm
-	PUBLIC $ENV{PLUGIN_SUBMODULE}/plugin-c
+	PUBLIC $ENV{PLUGIN_FULL_PATH}/plugin-c
 	PUBLIC $ENV{LOCAL_LIB}/proto
 	PUBLIC $ENV{NODE_DIR}/plugin-c
 	PUBLIC $ENV{NODE_DIR}/vm

flake.nix

@@ -89,7 +89,7 @@
             postPatch = ''
               substituteInPlace ./cmake/node/CMakeLists.txt \
                 --replace 'set(K_LIB ''${K_BIN}/../lib)' 'set(K_LIB ${k}/lib)'
-              substituteInPlace ./kevm \
+              substituteInPlace ./bin/kevm \
                 --replace 'execute python3 -m kevm_pyk' 'execute ${final.kevm-pyk}/bin/kevm-pyk'
             '';
 

abi.md renamed to include/kframework/abi.md

@@ -385,10 +385,6 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
 
     rule #getValue( #bytes4( X )) => X       requires #rangeUInt(32,  X)
     rule #getValue(#bytes32( X )) => X       requires #rangeUInt(256, X)
-
-    syntax Int ::= #ceil32 ( Int ) [macro]
- // --------------------------------------
-    rule #ceil32(N) => (N up/Int 32) *Int 32
 ```
 
 ### ABI Event Logs

asm.md renamed to include/kframework/asm.md

@@ -25,6 +25,10 @@ Claims should always use `#bufStrict` in LHS and `#buf` in RHS.
     syntax ByteArray ::= #bufStrict ( Int , Int ) [function]
     syntax ByteArray ::= #buf ( Int , Int ) [function, functional, smtlib(buf)]
 
+    syntax Int ::= #ceil32 ( Int ) [macro]
+ // --------------------------------------
+    rule #ceil32(N) => (N up/Int 32) *Int 32
+
 endmodule
 
 module BUF

buf.md renamed to include/kframework/buf.md

@@ -1,5 +1,5 @@
 requires "evm.md"
-requires "edsl.md"
+requires "buf.md"
 requires "int-simplification.k"
 
 module LEMMAS [symbolic]
@@ -83,21 +83,21 @@ module LEMMAS [symbolic]
 
     // #range
 
-    rule #range(_, _, K) => 
-         .ByteArray 
+    rule #range(_, _, K) =>
+         .ByteArray
       requires K <=Int 0 [simplification]
 
-    rule #range(M [ N := BUF:ByteArray ], L, K) => 
-         #let W = minInt(K, N -Int L) #in #range(M, L, W) ++ #range(M [ N := BUF ], N, K -Int W) 
+    rule #range(M [ N := BUF:ByteArray ], L, K) =>
+         #let W = minInt(K, N -Int L) #in #range(M, L, W) ++ #range(M [ N := BUF ], N, K -Int W)
       requires 0 <Int K andBool L <Int N [simplification]
 
-    rule #range(M [ N := BUF:ByteArray ], L, K) => 
+    rule #range(M [ N := BUF:ByteArray ], L, K) =>
            #let S = L -Int N #in
            #let W = minInt(K, #sizeByteArray(BUF) -Int S) #in
            BUF [ S .. W ] ++ #range(M, N +Int #sizeByteArray(BUF), K -Int W)
       requires 0 <Int K andBool N <=Int L andBool L <=Int N +Int #sizeByteArray(BUF) [simplification]
 
-    rule #range(M [ N := BUF:ByteArray ], L, K) => #range(M, L, K) 
+    rule #range(M [ N := BUF:ByteArray ], L, K) => #range(M, L, K)
       requires 0 <Int K andBool N +Int #sizeByteArray(BUF) <=Int L [simplification]
 
     rule #range( M [ N1 := BUF1:ByteArray ] [ N2 := BUF2:ByteArray ], L, K ) =>
@@ -151,7 +151,7 @@ endmodule
 
 module LEMMAS-JAVA [symbolic, kast]
     imports EVM
-    imports EDSL
+    imports BUF
     imports K-REFLECTION
 
   // ########################
@@ -273,7 +273,7 @@ endmodule
 module LEMMAS-HASKELL [symbolic, kore]
     imports INT-SYMBOLIC
     imports EVM
-    imports EDSL
+    imports BUF
 
   // ########################
   // Word Reasoning
@@ -405,7 +405,7 @@ module LEMMAS-HASKELL [symbolic, kore]
     rule BA:ByteArray   ==K #buf(32, DATA) => #buf(32, DATA) ==K              BA                                       [simplification, concrete(BA)]
     rule #buf(32, DATA) ==K BA:ByteArray   =>          DATA  ==Int #asInteger(BA) requires #sizeByteArray(BA) <=Int 32 [simplification, concrete(BA)]
 
-    rule #range(M, N1 +Int N2, K) => #range(#range(M, N2, #sizeByteArray(M) -Int N2), N1, K) 
+    rule #range(M, N1 +Int N2, K) => #range(#range(M, N2, #sizeByteArray(M) -Int N2), N1, K)
       requires 0 <=Int N1 andBool 0 <=Int N2
       [simplification, concrete(N2), concrete(M)]
 

data.md renamed to include/kframework/data.md

@@ -2,7 +2,7 @@ Parsing/Unparsing
 =================
 
 ```k
-requires "krypto.md"
+requires "plugin/krypto.md"
 requires "evm-types.md"
 requires "json-rpc.md"
 ```

driver.md renamed to include/kframework/driver.md

@@ -1,7 +1,7 @@
 diff --git a/kevm b/kevm
 index b77303c..9770f29 100755
---- a/kevm
-+++ b/kevm
+--- a/bin/kevm
++++ b/bin/kevm
 @@ -96,9 +96,6 @@ run_kompile() {
                     if [[ "$(uname -s)" == 'Linux' ]]; then
                         kompile_opts+=( -ccopt -lprocps )