Calculate transactionsRoot (#537)

* web3.md: Create rlpEncodeTransaction * Transactions Root * Small 'fix' to #nibbleize * Add firefly_getTxRoot * Tests for transactionsRoot
runtimeverification · Nov 6, 2019 · 061d899 · 061d899
1 parent 05e76b7
commit 061d899
Show file tree

Hide file tree

Showing 8 changed files with 173 additions and 27 deletions.
diff --git a/data.md b/data.md
@@ -1090,7 +1090,7 @@ Merkle Tree Aux Functions
     syntax ByteArray ::= #nibbleize ( ByteArray ) [function]
                        | #byteify   ( ByteArray ) [function]
  // --------------------------------------------------------
-    rule #nibbleize ( B ) => (    #asByteStack ( ( B [ 0 ] /Int 16 ) *Int 256 )[0 .. 1]
+    rule #nibbleize ( B ) => (      #asByteStack ( B [ 0 ] /Int 16 )[0 .. 1]
                                ++ ( #asByteStack ( B [ 0 ] %Int 16 )[0 .. 1] )
                              ) ++ #nibbleize ( B[1 .. #sizeByteArray(B) -Int 1] )
       requires #sizeByteArray( B ) >Int 0

diff --git a/tests/web3/firefly_getTxRoot.expected.json b/tests/web3/firefly_getTxRoot.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":true},{"jsonrpc":"2.0","id":3,"result":"0x2c11d46cf3df0566ee4b6c49c8dcc1197ec796dbbf267b4d03eacd5ada85f469"},{"jsonrpc":"2.0","id":4,"result":{"transactionsRoot":"0xaa980c3fa58e18367f9db477bc59fabd392c6f78cd2f8f8880c3401c786bfc07"}}]
diff --git a/tests/web3/firefly_getTxRoot.in.json b/tests/web3/firefly_getTxRoot.in.json
@@ -0,0 +1,37 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "balance":"0x56bc75e2d63100000"
+    }]
+},
+{
+    "jsonrpc":"2.0",
+    "id":2,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xf9eaf090058471f8ddb294ddeae71ff056b631420e6bdce27d90f3c1a8c74124",
+        "balance":"0x56bc75e2d63100000"
+    }]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 3,
+  "method": "eth_sendTransaction",
+  "params": [
+    {
+      "from": "0x911392821a6B8a3e0bD8078fC7403E04C3ad2416",
+      "to": "0x0093Ffb8D72408c1ab2547505A9914F0cF1F1298",
+      "value": "0x500",
+      "gasPrice": "0x4a817c800"
+    }
+  ]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 4,
+  "method": "firefly_getTxRoot",
+  "params": []
+}]
diff --git a/tests/web3/firefly_getTxRootCreate.expected.json b/tests/web3/firefly_getTxRootCreate.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":3,"result":"0x259f3f7dcd8df7aca8d214567b5f46ebd1325ee0502645a81cc6ba3b213a217b"},{"jsonrpc":"2.0","id":4,"result":{"transactionsRoot":"0x1e133bf205d1731e25e31f31f9b20271474ab937f88eec84c94a60a21fce15bf"}}]
diff --git a/tests/web3/firefly_getTxRootCreate.in.json b/tests/web3/firefly_getTxRootCreate.in.json
@@ -0,0 +1,28 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "balance":"0x56bc75e2d63100000"
+    }]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 3,
+  "method": "eth_sendTransaction",
+  "params": [
+    {
+      "from": "0x911392821a6B8a3e0bD8078fC7403E04C3ad2416",
+      "gasPrice": "0x4a817c800",
+      "gas":"0x100000",
+      "data": "0x6080604052348015600f57600080fd5b5060868061001e6000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80636d4ce63c14602d575b600080fd5b6033604c565b6040805163ffffffff9092168252519081900360200190f35b602a9056fea265627a7a72315820c0bd34730815aaf15c03933af0d41b94653dfda48fd932e0bcd9c83bc61cd5fa64736f6c634300050b0032"
+    }
+  ]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 4,
+  "method": "firefly_getTxRoot",
+  "params": []
+}]
diff --git a/tests/web3/firefly_getTxRootMultiple.expected.json b/tests/web3/firefly_getTxRootMultiple.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":true},{"jsonrpc":"2.0","id":3,"result":"0x2c11d46cf3df0566ee4b6c49c8dcc1197ec796dbbf267b4d03eacd5ada85f469"},{"jsonrpc":"2.0","id":3,"result":"0xca695a665221172b29e5bc6632211bd48189bc4db6e84bed07747a2afe7dbf13"},{"jsonrpc":"2.0","id":4,"result":{"transactionsRoot":"0x70e62ce367e4adf7ea004e9a3faf62f5fddae3a70f3a6b17bf380d52e3309c93"}}]
diff --git a/tests/web3/firefly_getTxRootMultiple.in.json b/tests/web3/firefly_getTxRootMultiple.in.json
@@ -0,0 +1,50 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "balance":"0x56bc75e2d63100000"
+    }]
+},
+{
+    "jsonrpc":"2.0",
+    "id":2,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xf9eaf090058471f8ddb294ddeae71ff056b631420e6bdce27d90f3c1a8c74124",
+        "balance":"0x56bc75e2d63100000"
+    }]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 3,
+  "method": "eth_sendTransaction",
+  "params": [
+    {
+      "from": "0x911392821a6B8a3e0bD8078fC7403E04C3ad2416",
+      "to": "0x0093Ffb8D72408c1ab2547505A9914F0cF1F1298",
+      "value": "0x500",
+      "gasPrice": "0x4a817c800"
+    }
+  ]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 3,
+  "method": "eth_sendTransaction",
+  "params": [
+    {
+      "from": "0x0093Ffb8D72408c1ab2547505A9914F0cF1F1298",
+      "to": "0x911392821a6B8a3e0bD8078fC7403E04C3ad2416",
+      "value": "0x20000",
+      "gasPrice": "0x4a817c800"
+    }
+  ]
+},
+{
+  "jsonrpc": "2.0",
+  "id": 4,
+  "method": "firefly_getTxRoot",
+  "params": []
+}]
diff --git a/web3.md b/web3.md
@@ -319,6 +319,8 @@ WEB3 JSON RPC
          <method> "firefly_getCoverageData" </method>
     rule <k> #runRPCCall => #firefly_getStateRoot ... </k>
          <method> "firefly_getStateRoot" </method>
+    rule <k> #runRPCCall => #firefly_getTxRoot ... </k>
+         <method> "firefly_getTxRoot" </method>
 
     rule <k> #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... </k> [owise]
 
@@ -590,32 +592,7 @@ eth_sendTransaction
     syntax String ::= #hashSignedTx   ( Int ) [function]
                     | #hashUnsignedTx ( Int ) [function]
  // ----------------------------------------------------
-    rule [[ #hashSignedTx( TXID )
-         => Keccak256( #rlpEncodeLength(         #rlpEncodeWord( TXNONCE )
-                                         +String #rlpEncodeWord( GPRICE )
-                                         +String #rlpEncodeWord( GLIMIT )
-                                         +String #rlpEncodeAccount( ACCTTO )
-                                         +String #rlpEncodeWord( VALUE )
-                                         +String #rlpEncodeString( #unparseByteStack( DATA ) )
-                                         +String #rlpEncodeWord( V )
-                                         +String #rlpEncodeString( #unparseByteStack( R ) )
-                                         +String #rlpEncodeString( #unparseByteStack( S ) )
-                                       , 192
-                                       )
-                     )
-         ]]
-         <message>
-           <msgID> TXID </msgID>
-           <txNonce>    TXNONCE </txNonce>
-           <txGasPrice> GPRICE  </txGasPrice>
-           <txGasLimit> GLIMIT  </txGasLimit>
-           <to>         ACCTTO  </to>
-           <value>      VALUE   </value>
-           <data>       DATA    </data>
-           <sigR>       R       </sigR>
-           <sigS>       S       </sigS>
-           <sigV>       V       </sigV>
-         </message>
+    rule #hashSignedTx( TXID ) => Keccak256( #rlpEncodeTransaction( TXID ) )
 
     rule [[ #hashUnsignedTx( TXID )
          => Keccak256( #rlpEncodeLength(         #rlpEncodeWord( TXNONCE )
@@ -1217,6 +1194,34 @@ Helper Funcs
            <code>    CODE    </code>
            ...
          </account>
+
+    syntax String ::= #rlpEncodeTransaction( Int ) [function]
+ // ---------------------------------------------------------
+    rule [[ #rlpEncodeTransaction( TXID )
+         => #rlpEncodeLength(         #rlpEncodeWord( TXNONCE )
+                              +String #rlpEncodeWord( GPRICE )
+                              +String #rlpEncodeWord( GLIMIT )
+                              +String #rlpEncodeAccount( ACCTTO )
+                              +String #rlpEncodeWord( VALUE )
+                              +String #rlpEncodeString( #unparseByteStack( DATA ) )
+                              +String #rlpEncodeWord( V )
+                              +String #rlpEncodeString( #unparseByteStack( R ) )
+                              +String #rlpEncodeString( #unparseByteStack( S ) )
+                            , 192
+                            )
+         ]]
+         <message>
+           <msgID> TXID </msgID>
+           <txNonce>    TXNONCE </txNonce>
+           <txGasPrice> GPRICE  </txGasPrice>
+           <txGasLimit> GLIMIT  </txGasLimit>
+           <to>         ACCTTO  </to>
+           <value>      VALUE   </value>
+           <data>       DATA    </data>
+           <sigR>       R       </sigR>
+           <sigS>       S       </sigS>
+           <sigV>       V       </sigV>
+         </message>
 ```
 
 State Root
@@ -1239,6 +1244,29 @@ State Root
     syntax KItem ::= "#firefly_getStateRoot"
  // ----------------------------------------
     rule <k> #firefly_getStateRoot => #sendResponse("result": { "stateRoot" : "0x" +String Keccak256( #rlpEncodeMerkleTree( #stateRoot ) ) } ) ... </k>
+```
+
+Transactions Root
+-----------------
+
+```k
+    syntax MerkleTree ::= "#transactionsRoot" [function]
+ // ----------------------------------------------------
+    rule #transactionsRoot => MerkleUpdateMap( .MerkleTree, #transactionsMap )
+
+    syntax Map ::= "#transactionsMap"         [function]
+                 | #transactionsMapAux( Int ) [function]
+ // ----------------------------------------------------
+    rule #transactionsMap => #transactionsMapAux( 0 )
+
+    rule #transactionsMapAux( _ )    => .Map [owise]
+    rule [[ #transactionsMapAux( I ) => #parseByteStackRaw( #rlpEncodeWord( I ) )[0 .. 1] |-> #rlpEncodeTransaction( { TXLIST[ I ] }:>Int ) #transactionsMapAux( I +Int 1 ) ]]
+         <txOrder> TXLIST </txOrder>
+      requires size(TXLIST) >Int I
+
+    syntax KItem ::= "#firefly_getTxRoot"
+ // -------------------------------------
+    rule <k> #firefly_getTxRoot => #sendResponse("result": { "transactionsRoot" : "0x" +String Keccak256( #rlpEncodeMerkleTree( #transactionsRoot ) ) } ) ... </k>
 
 endmodule
 ```
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":true},{"jsonrpc":"2.0","id":3,"result":"0x2c11d46cf3df0566ee4b6c49c8dcc1197ec796dbbf267b4d03eacd5ada85f469"},{"jsonrpc":"2.0","id":4,"result":{"transactionsRoot":"0xaa980c3fa58e18367f9db477bc59fabd392c6f78cd2f8f8880c3401c786bfc07"}}]