Data.md refactoring (#632)

* data: Factor out Word operations, WordStack, ByteArray, and Account into evm-types.md

data,evm-types: Move #addr from data to evm-types

* data,evm: Move M3:2048 bloomfilter from data.md to evm.md, the only place it is used

* data,driver: Move #removeZeros from data to driver, the only place it is used

* data,serialization: Move various helpers from data to serialization

* data,evm: Move #lookup to evm, next to the opcode that uses it

* data,web3: Move JSON and JSON-RPC modules into json.md

data,json: move JSONKEY ::= Int to JSON module

* data: Move parsing/unparsing, rlp, and merkle tree stuff to serialization.md

* Update concrete-rules.txt files

* tests/interactive/sumTo10.evm.parse-expected: Change EVM-DATA to EVM-TYPES

* evm,evm-types: Move #lookup to EVM-TYPES

Author: gtrepta

Makefile

@@ -153,7 +153,7 @@ MAIN_MODULE    := ETHEREUM-SIMULATION
 SYNTAX_MODULE  := $(MAIN_MODULE)
 export MAIN_DEFN_FILE := driver
 
-k_files       := driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3.k asm.k state-loader.k
+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
 EXTRA_K_FILES += $(MAIN_DEFN_FILE).k
 ALL_K_FILES   := $(k_files) $(EXTRA_K_FILES)
 

data.md

@@ -401,6 +401,18 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
          </account>
 ```
 
+-   `#removeZeros` removes any entries in a map with zero values.
+
+```k
+    syntax Map ::= #removeZeros ( Map ) [function]
+                 | #removeZeros ( List , Map ) [function, klabel(#removeZerosAux)]
+ // ------------------------------------------------------------------------------
+    rule #removeZeros( M )                                   => #removeZeros(Set2List(keys(M)), M)
+    rule #removeZeros( .List, .Map )                         => .Map
+    rule #removeZeros( ListItem(KEY) L, KEY |-> 0 REST )     => #removeZeros(L, REST)
+    rule #removeZeros( ListItem(KEY) L, KEY |-> VALUE REST ) => KEY |-> VALUE #removeZeros(L, REST) requires VALUE =/=K 0
+```
+
 Here we check the other post-conditions associated with an EVM test.
 
 ```k

driver.md

@@ -709,6 +709,22 @@ After executing a transaction, it's necessary to have the effect of the substate
     rule #bloomFilter(ListItem(WS:ByteArray) L, B) => #bloomFilter(L, B |Int M3:2048(WS))
 ```
 
+- `M3:2048` computes the 2048-bit hash of a log entry in which exactly 3 bits are set. This is used to compute the Bloom filter of a log entry.
+
+```k
+    syntax Int ::= "M3:2048" "(" ByteArray ")" [function]
+ // -----------------------------------------------------
+    rule M3:2048(WS) => setBloomFilterBits(#parseByteStack(Keccak256(#unparseByteStack(WS))))
+
+    syntax Int ::= setBloomFilterBits(ByteArray) [function]
+ // -------------------------------------------------------
+    rule setBloomFilterBits(HASH) => (1 <<Int getBloomFilterBit(HASH, 0)) |Int (1 <<Int getBloomFilterBit(HASH, 2)) |Int (1 <<Int getBloomFilterBit(HASH, 4))
+
+    syntax Int ::= getBloomFilterBit(ByteArray, Int) [function]
+ // -----------------------------------------------------------
+    rule getBloomFilterBit(X, I) => #asInteger(X [ I .. 2 ]) %Int 2048
+```
+
 EVM Programs
 ============
 

evm-types.md

@@ -0,0 +1,76 @@
+### JSON Formatting
+
+The JSON format is used extensively for communication in the Ethereum circles.
+Writing a JSON-ish parser in K takes 6 lines.
+
+```k
+module JSON
+    imports INT
+    imports STRING
+    imports BOOL
+
+    syntax JSONs   ::= List{JSON,","}      [klabel(JSONs)      , symbol]
+    syntax JSONKey ::= String
+    syntax JSON    ::= "null"              [klabel(JSONnull)   , symbol]
+                     | String | Int | Bool
+                     | JSONKey ":" JSON    [klabel(JSONEntry)  , symbol]
+                     | "{" JSONs "}"       [klabel(JSONObject) , symbol]
+                     | "[" JSONs "]"       [klabel(JSONList)   , symbol]
+ // --------------------------------------------------------------------
+```
+
+**TODO**: Adding `Int` to `JSONKey` is a hack to make certain parts of semantics easier.
+
+```k
+    syntax JSONKey ::= Int
+ // ----------------------
+
+endmodule
+```
+
+JSON-RPC
+--------
+
+```k
+module JSON-RPC
+    imports K-IO
+    imports LIST
+    imports JSON
+
+    configuration
+      <json-rpc>
+        <web3socket> $SOCK:Int </web3socket>
+        <web3clientsocket> 0:IOInt </web3clientsocket>
+        <web3request>
+          <jsonrpc> "":JSON </jsonrpc>
+          <callid> 0:JSON </callid>
+          <method> "":JSON </method>
+          <params> [ .JSONs ] </params>
+          <batch> undef </batch>
+        </web3request>
+        <web3response> .List </web3response>
+      </json-rpc>
+
+    syntax JSON ::= "undef" [klabel(JSON-RPCundef), symbol]
+ // -------------------------------------------------------
+
+    syntax Bool ::= isProperJson     ( JSON  ) [function]
+                  | isProperJsonList ( JSONs ) [function]
+ // -----------------------------------------------------
+    rule isProperJson(_) => false [owise]
+
+    rule isProperJson(null) => true
+
+    rule isProperJson(_:Int)    => true
+    rule isProperJson(_:Bool)   => true
+    rule isProperJson(_:String) => true
+
+    rule isProperJson(_:JSONKey : J) => isProperJson(J)
+
+    rule isProperJson([ JS ]) => isProperJsonList(JS)
+    rule isProperJson({ JS }) => isProperJsonList(JS)
+
+    rule isProperJsonList(.JSONs) => true
+    rule isProperJsonList(J, JS)  => isProperJson(J) andBool isProperJsonList(JS)
+endmodule
+```