Batch processing of web3 requests (#441)

* tests

* web3: batch processing

* web3: fix everett's comment

tests/web3/batch_all_notification.in.json

@@ -0,0 +1,13 @@
+[{
+  "jsonrpc": "2.0",
+  "method": "net_version",
+  "params": []
+},{
+  "jsonrpc": "2.0",
+  "method": "net_version",
+  "params": []
+},{
+  "jsonrpc": "2.0",
+  "method": "net_version",
+  "params": []
+}]

tests/web3/batch_empty_array.in.json

@@ -0,0 +1 @@
+[]

tests/web3/batch_empty_array.out.json

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"Invalid Request"}}

tests/web3/batch_invalid_array.in.json

@@ -0,0 +1 @@
+[1]

tests/web3/batch_invalid_array.out.json

@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"Invalid Request"}}]

tests/web3/batch_invalid_array_2.in.json

@@ -0,0 +1 @@
+[1,2]

tests/web3/batch_invalid_array_2.out.json

@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"Invalid Request"}},{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"Invalid Request"}}]

tests/web3/batch_partial_notification.in.json

@@ -0,0 +1,10 @@
+[{
+  "jsonrpc": "2.0",
+  "method": "net_version",
+  "params": []
+},{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "method": "net_version",
+  "params": []
+}]

tests/web3/batch_partial_notification.out.json

@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":"28346"}]

tests/web3/batch_partially_valid.in.json

@@ -0,0 +1,6 @@
+[{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "method": "net_version",
+  "params": []
+},{}]

tests/web3/batch_partially_valid.out.json

@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":"28346"},{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"Invalid Request"}}]

web3.md

@@ -22,7 +22,9 @@ module WEB3
           <callid> 0:JSON </callid>
           <method> "":JSON </method>
           <params> [ .JSONList ] </params>
+          <batch> undef </batch>
         </web3request>
+        <web3response> .List </web3response>
       </kevm-client>
 
     syntax JSON ::= Int | Bool | "null" | "undef"
@@ -53,6 +55,7 @@ module WEB3
  // -----------------------------
     rule <k> getRequest() => #loadRPCCall(#getRequest(SOCK)) ... </k>
          <web3clientsocket> SOCK </web3clientsocket>
+         <batch> _ => undef </batch>
 
     syntax IOJSON ::= #getRequest(Int) [function, hook(JSON.read)]
  // --------------------------------------------------------------
@@ -71,15 +74,56 @@ module WEB3
     rule <k> #loadRPCCall(#EOF) => #shutdownWrite(SOCK) ~> #close(SOCK) ~> accept() ... </k>
          <web3clientsocket> SOCK </web3clientsocket>
 
+    rule <k> #loadRPCCall([ _, _ ] #as J) => #loadFromBatch ... </k>
+         <batch> _ => J </batch>
+         <web3response> _ => .List </web3response>
+
+    rule <k> #loadRPCCall(_:String #Or null #Or _:Int #Or [ .JSONList ]) => #sendResponse("error": {"code": -32600, "message": "Invalid Request"}) ... </k>
+         <callid> _ => null </callid>
+
+    syntax KItem ::= "#loadFromBatch"
+ // ---------------------------------
+    rule <k> #loadFromBatch ~> _ => #loadRPCCall(J) </k>
+         <batch> [ J , JS => JS ] </batch>
+
+    rule <k> #loadFromBatch ~> _ => #putResponse(List2JSON(RESPONSE), SOCK) ~> getRequest() </k>
+         <batch> [ .JSONList ] </batch>
+         <web3clientsocket> SOCK </web3clientsocket>
+         <web3response> RESPONSE </web3response>
+      requires size(RESPONSE) >Int 0
+
+    rule <k> #loadFromBatch ~> _ => getRequest() </k>
+         <batch> [ .JSONList ] </batch>
+         <web3response> .List </web3response>
+
+    syntax JSON ::= List2JSON(List)           [function]
+                  | List2JSON(List, JSONList) [function, klabel(List2JSONAux)]
+ // --------------------------------------------------------------------------
+    rule List2JSON(L) => List2JSON(L, .JSONList)
+
+    rule List2JSON(L ListItem(J), JS) => List2JSON(L, (J, JS))
+    rule List2JSON(.List, JS) => [ JS ]
+
     syntax KItem ::= #sendResponse( JSON )
  // --------------------------------------
     rule <k> #sendResponse(J) ~> _ => #putResponse({ "jsonrpc": "2.0", "id": CALLID, J }, SOCK) ~> getRequest() </k>
          <callid> CALLID </callid>
          <web3clientsocket> SOCK </web3clientsocket>
+         <batch> undef </batch>
       requires CALLID =/=K undef
 
     rule <k> #sendResponse(_) ~> _ => getRequest() </k>
          <callid> undef </callid>
+         <batch> undef </batch>
+
+    rule <k> #sendResponse(J) ~> _ => #loadFromBatch </k>
+         <callid> CALLID </callid>
+         <batch> [ _ ] </batch>
+         <web3response>... .List => ListItem({ "jsonrpc": "2.0", "id": CALLID, J }) </web3response>
+
+    rule <k> #sendResponse(_) ~> _ => #loadFromBatch </k>
+         <callid> undef </callid>
+         <batch> [ _ ] </batch>
 
     syntax KItem ::= "#checkRPCCall"
  // --------------------------------