implement EXTCODEHASH in node. (#403)

* deps/plugin: update plugin submodule

* evm, evm-node: extcodehash in node mode

* don't build ocaml node

Author: dwightguth

Makefile

@@ -241,7 +241,7 @@ $(DEFN_DIR)/ocaml/$(MAIN_DEFN_FILE)-kompiled/constants.$(EXT): $(ocaml_files)
 	eval $$(opam config env) \
 	    && $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) \
 	                        --syntax-module $(SYNTAX_MODULE) $(DEFN_DIR)/ocaml/$(MAIN_DEFN_FILE).k \
-	                        --hook-namespaces "KRYPTO BLOCKCHAIN" --gen-ml-only -O3 --non-strict \
+	                        --hook-namespaces "KRYPTO" --gen-ml-only -O3 --non-strict \
 	                        --directory $(DEFN_DIR)/ocaml -I $(DEFN_DIR)/ocaml $(KOMPILE_OPTS) \
 	    && cd $(DEFN_DIR)/ocaml/$(MAIN_DEFN_FILE)-kompiled \
 	    && ocamlfind $(OCAMLC) -c -g constants.ml -package gmp -package zarith -safe-string
@@ -254,9 +254,9 @@ $(DEFN_DIR)/ocaml/$(MAIN_DEFN_FILE)-kompiled/plugin/semantics.$(LIBEXT): $(wildc
 	    && ocaml-protoc $(PLUGIN_SUBMODULE)/plugin/proto/*.proto -ml_out $(dir $@) \
 	    && cd $(dir $@) \
 	        && ocamlfind $(OCAMLC) -c -g -I $(CURDIR)/$(DEFN_DIR)/ocaml/$(MAIN_DEFN_FILE)-kompiled \
-	                               msg_types.mli msg_types.ml msg_pb.mli msg_pb.ml apiVersion.ml world.mli world.ml caching.mli caching.ml BLOCKCHAIN.ml KRYPTO.ml \
+	                               KRYPTO.ml \
 	                               -package cryptokit -package secp256k1 -package bn128 -package ocaml-protoc -safe-string -thread \
-	        && ocamlfind $(OCAMLC) -a -o semantics.$(LIBEXT) KRYPTO.$(EXT) msg_types.$(EXT) msg_pb.$(EXT) apiVersion.$(EXT) world.$(EXT) caching.$(EXT) BLOCKCHAIN.$(EXT) -thread \
+	        && ocamlfind $(OCAMLC) -a -o semantics.$(LIBEXT) KRYPTO.$(EXT) -thread \
 	        && ocamlfind remove ethereum-semantics-plugin-ocaml \
 	        && ocamlfind install ethereum-semantics-plugin-ocaml $(PLUGIN_SUBMODULE)/plugin/META semantics.* *.cmi *.$(EXT)
 

deps/plugin

@@ -22,7 +22,7 @@ Because the same account may be loaded more than once, implementations of this i
 -   Empty code is detected without lazy evaluation by means of checking the code hash, and therefore will always be represented in the `<code>` cell as `.WordStack`.
 
 ```{.k .node}
-    syntax AccountCode ::= "#unloaded"
+    syntax AccountCode ::= #unloaded(Int)
 ```
 
 -   `#getBalance` returns the balance of an account that exists based on its integer address.
@@ -31,9 +31,10 @@ Because the same account may be loaded more than once, implementations of this i
 -   `#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)]
- // -------------------------------------------------------------------------
+    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)]
@@ -51,7 +52,7 @@ Because the same account may be loaded more than once, implementations of this i
           => <account>
                <acctID> ACCT </acctID>
                <balance> #getBalance(ACCT) </balance>
-               <code> #if #isCodeEmpty(ACCT) #then .WordStack #else #unloaded #fi </code>
+               <code> #if #isCodeEmpty(ACCT) #then .WordStack #else #unloaded(#getCodeHash(ACCT)) #fi </code>
                <storage> .Map </storage>
                <origStorage> .Map </origStorage>
                <nonce> #getNonce(ACCT) </nonce>
@@ -102,7 +103,7 @@ Because the same account may be loaded more than once, implementations of this i
     rule <k> #lookupCode ACCT => . ... </k>
          <account>
            <acctID> ACCT </acctID>
-           <code> #unloaded => #parseByteStackRaw(#getCode(ACCT)) </code>
+           <code> #unloaded(_) => #parseByteStackRaw(#getCode(ACCT)) </code>
            ...
          </account>
 
@@ -127,6 +128,17 @@ Because the same account may be loaded more than once, implementations of this i
     rule <k> BLOCKHASH N => 0                ~> #push ... </k> <mode> NORMAL </mode> requires N  <Int 0  orBool N >=Int 256
 ```
 
+```{.k .node}
+    rule <k> EXTCODEHASH ACCT => HASH ~> #push ... </k>
+         <account>
+           <acctID> ACCT </acctID>
+           <code> #unloaded(HASH) </code>
+           <nonce> NONCE </nonce>
+           <balance> BAL </balance>
+           ...
+         </account>
+```
+
 ### 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.

evm-node.md

@@ -1134,19 +1134,17 @@ For now, I assume that they instantiate an empty account and use the empty data.
  // ----------------------------------
 ```
 
-```{.k .standalone}
+```k
     rule <k> EXTCODEHASH ACCT => keccak(CODE) ~> #push ... </k>
          <account>
            <acctID> ACCT </acctID>
-           <code> CODE </code>
+           <code> CODE:WordStack </code>
            <nonce> NONCE </nonce>
            <balance> BAL </balance>
            ...
          </account>
       requires notBool #accountEmpty(CODE, NONCE, BAL)
-```
 
-```k
      rule <k> EXTCODEHASH ACCT => 0 ~> #push ... </k>
          <account>
            <acctID> ACCT </acctID>