From e15f5e92d2ae77151c1a7a29c1c5384d767b2b4d Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Thu, 30 Jul 2020 16:56:07 -0400 Subject: [PATCH 1/9] move protobuf files to plugin-c dir Idea: reserve /plugin dir for K files --- Makefile | 2 +- {plugin => plugin-c}/proto/VERSION | 0 {plugin => plugin-c}/proto/msg.proto | 0 3 files changed, 1 insertion(+), 1 deletion(-) rename {plugin => plugin-c}/proto/VERSION (100%) rename {plugin => plugin-c}/proto/msg.proto (100%) diff --git a/Makefile b/Makefile index 92b101bc2..97ae8f267 100644 --- a/Makefile +++ b/Makefile @@ -20,7 +20,7 @@ CPPFLAGS += --std=c++14 $(INCLUDES) .PHONY: build libcryptopp libff libsecp256k1 build: client-c/json.o client-c/main.o plugin-c/blake2.o plugin-c/blockchain.o plugin-c/crypto.o plugin-c/plugin_util.o plugin-c/world.o -plugin-c/blockchain.o: plugin/proto/msg.pb.h +plugin-c/blockchain.o: plugin-c/proto/msg.pb.h %.pb.h: %.proto protoc --cpp_out=. $< diff --git a/plugin/proto/VERSION b/plugin-c/proto/VERSION similarity index 100% rename from plugin/proto/VERSION rename to plugin-c/proto/VERSION diff --git a/plugin/proto/msg.proto b/plugin-c/proto/msg.proto similarity index 100% rename from plugin/proto/msg.proto rename to plugin-c/proto/msg.proto From 52910d952ccba93f8f1f1e499d9467a8f1734d7d Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Thu, 30 Jul 2020 17:08:45 -0400 Subject: [PATCH 2/9] initial import of krypto.md file --- plugin/krypto.md | 55 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 plugin/krypto.md diff --git a/plugin/krypto.md b/plugin/krypto.md new file mode 100644 index 000000000..f77255b54 --- /dev/null +++ b/plugin/krypto.md @@ -0,0 +1,55 @@ +Cryptographic Primitives +======================== + +Here we implement the various cryptographic primitives needed for KEVM. + +```k +module KRYPTO + imports STRING-SYNTAX + imports INT-SYNTAX + imports LIST +``` + +- `Keccak256` takes a string and returns a 64-character hex-encoded string of the 32-byte keccak256 hash of the string. +- `Sha256` takes a String and returns a 64-character hex-encoded string of the 32-byte SHA2-256 hash of the string. +- `RipEmd160` takes a String and returns a 40-character hex-encoded string of the 20-byte RIPEMD160 hash of the string. +- `ECDSARecover` takes a 32-character byte string of a message, v, r, s of the signed message and returns the 64-character public key used to sign the message. +- `ECDSASign` takes a 32-character byte string of a message hash, a 32-character byte string of a private key, and returns the 65 byte hex-encoded signature in [r,s,v] form +- `ECDSAPubKey` takes a 32-character byte string of a private key, and returns the 64 byte hex-encoded public key + See [this StackOverflow post](https://ethereum.stackexchange.com/questions/15766/what-does-v-r-s-in-eth-gettransactionbyhash-mean) for some information about v, r, and s. + +In all functions above, input `String` is interpreted as byte array, e.g. it is NOT hex-encoded. + +```k + syntax String ::= Keccak256 ( String ) [function, hook(KRYPTO.keccak256)] + | ECDSARecover ( String , Int , String , String ) [function, hook(KRYPTO.ecdsaRecover)] + | Sha256 ( String ) [function, hook(KRYPTO.sha256)] + | RipEmd160 ( String ) [function, hook(KRYPTO.ripemd160)] + | ECDSASign ( String, String ) [function, hook(KRYPTO.ecdsaSign)] + | ECDSAPubKey ( String ) [function, hook(KRYPTO.ecdsaPubKey)] + | Blake2Compress ( String ) [function, hook(KRYPTO.blake2compress)] + // --------------------------------------------------------------------------------------------------------- +``` + +The BN128 elliptic curve is defined over 2-dimensional points over the fields of zero- and first-degree polynomials modulo a large prime. (x, y) is a point on G1, whereas (x1 x x2, y1 x y2) is a point on G2, in which x1 and y1 are zero-degree coefficients and x2 and y2 are first-degree coefficients. In each case, (0, 0) is used to represent the point at infinity. + +- `BN128Add` adds two points in G1 together, +- `BN128Mul` multiplies a point in G1 by a scalar. +- `BN128AtePairing` accepts a list of points in G1 and a list of points in G2 and returns whether the sum of the product of the discrete logarithm of the G1 points multiplied by the discrete logarithm of the G2 points is equal to zero. +- `isValidPoint` takes a point in either G1 or G2 and validates that it actually falls on the respective elliptic curve. + +```k + syntax G1Point ::= "(" Int "," Int ")" [prefer] + syntax G2Point ::= "(" Int "x" Int "," Int "x" Int ")" + syntax G1Point ::= BN128Add(G1Point, G1Point) [function, hook(KRYPTO.bn128add)] + | BN128Mul(G1Point, Int) [function, hook(KRYPTO.bn128mul)] + // ------------------------------------------------------------------------------- + + syntax Bool ::= BN128AtePairing(List, List) [function, hook(KRYPTO.bn128ate)] + // ----------------------------------------------------------------------------- + + syntax Bool ::= isValidPoint(G1Point) [function, hook(KRYPTO.bn128valid)] + | isValidPoint(G2Point) [function, klabel(isValidG2Point), hook(KRYPTO.bn128g2valid)] + // --------------------------------------------------------------------------------------------------- +endmodule +``` From f6daddf0dde78228d07f4f9f7925e57dfa0e0475 Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Thu, 30 Jul 2020 18:58:38 -0400 Subject: [PATCH 3/9] krypto.md: update documentation, add hooked hash functions --- plugin/krypto.md | 61 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 51 insertions(+), 10 deletions(-) diff --git a/plugin/krypto.md b/plugin/krypto.md index f77255b54..6bc016fd3 100644 --- a/plugin/krypto.md +++ b/plugin/krypto.md @@ -1,7 +1,7 @@ Cryptographic Primitives ======================== -Here we implement the various cryptographic primitives needed for KEVM. +Here we implement the various cryptographic primitives needed for various blockchain systems. ```k module KRYPTO @@ -10,27 +10,68 @@ module KRYPTO imports LIST ``` +Hash Functions +-------------- + +In hooked hash functions, `String` inputs are interpreted as byte arrays, i.e. they are NOT hex-encoded. +`String` outputs are interpreted differently depending on which class of hooked hash functions they belong to: + +- hex-encoded - return binary data as hex-encoded strings +- raw - return binary data as raw strings (i.e. NO hex-encoding) + +### Hooked Hash Functions with Hex Encoded Outputs + - `Keccak256` takes a string and returns a 64-character hex-encoded string of the 32-byte keccak256 hash of the string. -- `Sha256` takes a String and returns a 64-character hex-encoded string of the 32-byte SHA2-256 hash of the string. -- `RipEmd160` takes a String and returns a 40-character hex-encoded string of the 20-byte RIPEMD160 hash of the string. +- `Sha256` takes a string and returns a 64-character hex-encoded string of the 32-byte SHA2-256 hash of the string. +- `Sha512` takes a string and returns a 128-character hex-encoded string of the 64-byte SHA2-512 hash of the string. +- `Sha3_256` takes a string and returns 64-character hex-encoded string of the 32-byte SHA3-256 hash of the string. +- `RipEmd160` takes a string and returns a 40-character hex-encoded string of the 20-byte RIPEMD160 hash of the string. +- `Blake2Compress` takes a raw string containing a packed encoding of the arguments to the Blake2b compression + function F and returns a 128-character hex-encoded string of the 64-byte result from the compression function. + +```k + syntax String ::= Keccak256 ( String ) [function, hook(KRYPTO.keccak256)] + | Sha256 ( String ) [function, hook(KRYPTO.sha256)] + | Sha512 ( String ) [function, hook(KRYPTO.sha256)] + | "Sha3_256" "(" String ")" [function, hook(KRYPTO.sha3)] + | RipEmd160 ( String ) [function, hook(KRYPTO.ripemd160)] + | Blake2Compress ( String ) [function, hook(KRYPTO.blake2compress)] + // --------------------------------------------------------------------------------------------------------- +``` + +### Hooked Hash Functions with Raw Outputs + +These functions compute the same hash function as those named above except that they return a raw string. + +```k + syntax String ::= Keccak256raw ( String ) [function, hook(KRYPTO.keccak256raw)] + | Sha256raw ( String ) [function, hook(KRYPTO.sha256raw)] + | Sha512raw ( String ) [function, hook(KRYPTO.sha256raw)] + | "Sha3_256raw" "(" String ")" [function, hook(KRYPTO.sha3raw)] + | RipEmd160raw ( String ) [function, hook(KRYPTO.ripemd160raw)] + // ------------------------------------------------------------------------------------------------------- +``` + +ECDSA Functions +--------------- + +For hooked ECDSA functions, `String` inputs are interpreted as byte arrays, i.e. they are NOT hex-encoded. + - `ECDSARecover` takes a 32-character byte string of a message, v, r, s of the signed message and returns the 64-character public key used to sign the message. - `ECDSASign` takes a 32-character byte string of a message hash, a 32-character byte string of a private key, and returns the 65 byte hex-encoded signature in [r,s,v] form - `ECDSAPubKey` takes a 32-character byte string of a private key, and returns the 64 byte hex-encoded public key See [this StackOverflow post](https://ethereum.stackexchange.com/questions/15766/what-does-v-r-s-in-eth-gettransactionbyhash-mean) for some information about v, r, and s. -In all functions above, input `String` is interpreted as byte array, e.g. it is NOT hex-encoded. - ```k - syntax String ::= Keccak256 ( String ) [function, hook(KRYPTO.keccak256)] - | ECDSARecover ( String , Int , String , String ) [function, hook(KRYPTO.ecdsaRecover)] - | Sha256 ( String ) [function, hook(KRYPTO.sha256)] - | RipEmd160 ( String ) [function, hook(KRYPTO.ripemd160)] + syntax String ::= ECDSARecover ( String , Int , String , String ) [function, hook(KRYPTO.ecdsaRecover)] | ECDSASign ( String, String ) [function, hook(KRYPTO.ecdsaSign)] | ECDSAPubKey ( String ) [function, hook(KRYPTO.ecdsaPubKey)] - | Blake2Compress ( String ) [function, hook(KRYPTO.blake2compress)] // --------------------------------------------------------------------------------------------------------- ``` +BN128 Curve Functions +--------------------- + The BN128 elliptic curve is defined over 2-dimensional points over the fields of zero- and first-degree polynomials modulo a large prime. (x, y) is a point on G1, whereas (x1 x x2, y1 x y2) is a point on G2, in which x1 and y1 are zero-degree coefficients and x2 and y2 are first-degree coefficients. In each case, (0, 0) is used to represent the point at infinity. - `BN128Add` adds two points in G1 together, From eab8e6fc35ee798cba3efb438005420f80b16f55 Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Thu, 30 Jul 2020 18:59:20 -0400 Subject: [PATCH 4/9] krypto.md: add hash funcs that depend on custom libcrypto++ --- plugin/krypto.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/plugin/krypto.md b/plugin/krypto.md index 6bc016fd3..49ec574e6 100644 --- a/plugin/krypto.md +++ b/plugin/krypto.md @@ -52,6 +52,21 @@ These functions compute the same hash function as those named above except that // ------------------------------------------------------------------------------------------------------- ``` +### Other Hooked Hash Functions + +These hooked hash functions are broken on default Ubuntu installations because of a bug in `libcrypto++` package. +As such, we we hide them behind a separate tangle tag to avoid breaking projects that do not use them. + +- `Blake2b256` takes a string and returns a 64-character hex-encoded string of the 32-byte Blake2b256 hash of the string. +- `Blake2b256raw` takes a string and returns the 32-byte Blake2b256 hash of the string. + +```libcrypto-extra +```k + syntax String ::= Blake2b256 ( String ) [function, hook(KRYPTO.keccak256raw)] + | Blake2b256raw ( String ) [function, hook(KRYPTO.sha256raw)] + // ------------------------------------------------------------------------------------------------------- +``` + ECDSA Functions --------------- From 3d755b0778c08c5229daf57784d8659a011ad51e Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Mon, 3 Aug 2020 23:12:31 -0400 Subject: [PATCH 5/9] krypto.md: fix syntax error in markdown --- plugin/krypto.md | 1 - 1 file changed, 1 deletion(-) diff --git a/plugin/krypto.md b/plugin/krypto.md index 49ec574e6..79f40dae4 100644 --- a/plugin/krypto.md +++ b/plugin/krypto.md @@ -61,7 +61,6 @@ As such, we we hide them behind a separate tangle tag to avoid breaking projects - `Blake2b256raw` takes a string and returns the 32-byte Blake2b256 hash of the string. ```libcrypto-extra -```k syntax String ::= Blake2b256 ( String ) [function, hook(KRYPTO.keccak256raw)] | Blake2b256raw ( String ) [function, hook(KRYPTO.sha256raw)] // ------------------------------------------------------------------------------------------------------- From eef300e50eabab2ece1f0cc375d624a1d5e1c455 Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Mon, 3 Aug 2020 23:18:40 -0400 Subject: [PATCH 6/9] krypto.md: fix hook names --- plugin/krypto.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/plugin/krypto.md b/plugin/krypto.md index 79f40dae4..07020cc14 100644 --- a/plugin/krypto.md +++ b/plugin/krypto.md @@ -32,7 +32,7 @@ In hooked hash functions, `String` inputs are interpreted as byte arrays, i.e. t ```k syntax String ::= Keccak256 ( String ) [function, hook(KRYPTO.keccak256)] | Sha256 ( String ) [function, hook(KRYPTO.sha256)] - | Sha512 ( String ) [function, hook(KRYPTO.sha256)] + | Sha512 ( String ) [function, hook(KRYPTO.sha512)] | "Sha3_256" "(" String ")" [function, hook(KRYPTO.sha3)] | RipEmd160 ( String ) [function, hook(KRYPTO.ripemd160)] | Blake2Compress ( String ) [function, hook(KRYPTO.blake2compress)] @@ -46,7 +46,7 @@ These functions compute the same hash function as those named above except that ```k syntax String ::= Keccak256raw ( String ) [function, hook(KRYPTO.keccak256raw)] | Sha256raw ( String ) [function, hook(KRYPTO.sha256raw)] - | Sha512raw ( String ) [function, hook(KRYPTO.sha256raw)] + | Sha512raw ( String ) [function, hook(KRYPTO.sha512raw)] | "Sha3_256raw" "(" String ")" [function, hook(KRYPTO.sha3raw)] | RipEmd160raw ( String ) [function, hook(KRYPTO.ripemd160raw)] // ------------------------------------------------------------------------------------------------------- @@ -61,9 +61,9 @@ As such, we we hide them behind a separate tangle tag to avoid breaking projects - `Blake2b256raw` takes a string and returns the 32-byte Blake2b256 hash of the string. ```libcrypto-extra - syntax String ::= Blake2b256 ( String ) [function, hook(KRYPTO.keccak256raw)] - | Blake2b256raw ( String ) [function, hook(KRYPTO.sha256raw)] - // ------------------------------------------------------------------------------------------------------- + syntax String ::= Blake2b256 ( String ) [function, hook(KRYPTO.blake2b256)] + | Blake2b256raw ( String ) [function, hook(KRYPTO.blake2b256raw)] + // -------------------------------------------------------------------------------------------------------- ``` ECDSA Functions From d81e7603ce9efc40a549161d003f026ae5cd8f2a Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Thu, 13 Aug 2020 19:48:55 -0400 Subject: [PATCH 7/9] Makefile: add install target to copy K files --- Makefile | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 97ae8f267..1da8c3997 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,11 @@ plugin-c/blockchain.o: plugin-c/proto/msg.pb.h %.pb.h: %.proto protoc --cpp_out=. $< -.PHONY: clean +.PHONY: install clean +install: + @mkdir -p $(PREFIX) + cp plugin/* $(PREFIX) + clean: rm -rf */*.o */*/*.o plugin/proto/*.pb.* build deps/libff/build cd deps/secp256k1 && $(MAKE) clean From 82da6229d1eea9d5ffc984ff0889489aaa04e971 Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Sat, 29 Aug 2020 20:45:21 -0400 Subject: [PATCH 8/9] Makefile: update install target to copy to prefix subdir --- Makefile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 1da8c3997..cfff8a1a3 100644 --- a/Makefile +++ b/Makefile @@ -26,9 +26,11 @@ plugin-c/blockchain.o: plugin-c/proto/msg.pb.h protoc --cpp_out=. $< .PHONY: install clean + +PLUGIN_NAMESPACE := blockchain-k-plugin install: - @mkdir -p $(PREFIX) - cp plugin/* $(PREFIX) + @mkdir -p $(PREFIX)/$(PLUGIN_NAMESPACE) + cp plugin/* $(PREFIX)/$(PLUGIN_NAMESPACE) clean: rm -rf */*.o */*/*.o plugin/proto/*.pb.* build deps/libff/build From d393510bfbb9b2d7708b760434f004896e273e0d Mon Sep 17 00:00:00 2001 From: Stephen Skeirik <7319434+sskeirik@users.noreply.github.com> Date: Mon, 14 Sep 2020 15:03:23 -0400 Subject: [PATCH 9/9] Update Makefile install logic Co-authored-by: Everett Hildenbrandt --- Makefile | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index cfff8a1a3..55baa2766 100644 --- a/Makefile +++ b/Makefile @@ -27,10 +27,19 @@ plugin-c/blockchain.o: plugin-c/proto/msg.pb.h .PHONY: install clean +DESTDIR ?= +INSTALL_PREFIX ?= /usr/local +INSTALL_DIR := $(DESTDIR)$(INSTALL_PREFIX) +INSTALL_INCLUDE := $(INSTALL_DIR)/include/kframework + PLUGIN_NAMESPACE := blockchain-k-plugin -install: - @mkdir -p $(PREFIX)/$(PLUGIN_NAMESPACE) - cp plugin/* $(PREFIX)/$(PLUGIN_NAMESPACE) +K_SOURCES := krypto.md + +install: $(patsubst %, $(INSTALL_INCLUDE)/$(PLUGIN_NAMESPACE)/%, $(K_SOURCES)) + +$(INSTALL_INCLUDE)/$(PLUGIN_NAMESPACE)/%.md: plugin/%.md + @mkdir -p $(dir $@) + cp $< $@ clean: rm -rf */*.o */*/*.o plugin/proto/*.pb.* build deps/libff/build