stateRoot Implementation (#533)

* Add stateRoot * Add a test for stateRoot * Add more tests
runtimeverification · Nov 4, 2019 · 05e76b7 · 05e76b7
1 parent c1425a3
commit 05e76b7
Show file tree

Hide file tree

Showing 10 changed files with 146 additions and 0 deletions.
diff --git a/data.md b/data.md
@@ -1182,6 +1182,44 @@ Tree Root Helper Functions
     syntax MerkleTree ::= #storageRoot( Map ) [function]
  // ----------------------------------------------------
     rule #storageRoot( STORAGE ) => MerkleUpdateMap( .MerkleTree, #intMap2StorageMap( STORAGE ) )
+```
+
+### State Root
+
+```k
+    syntax Map ::= "#precompiledContracts" [function]
+ // -------------------------------------------------
+    rule #precompiledContracts
+      => #parseByteStackRaw( Hex2Raw( #unparseData( 1, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 2, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 3, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 4, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 5, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 6, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 7, 20 ) ) ) |-> #emptyContractRLP
+         #parseByteStackRaw( Hex2Raw( #unparseData( 8, 20 ) ) ) |-> #emptyContractRLP
+
+    syntax String ::= "#emptyContractRLP" [function]
+ // ------------------------------------------------
+    rule #emptyContractRLP => #rlpEncodeLength(         #rlpEncodeWord(0)
+                                                +String #rlpEncodeWord(0)
+                                                +String #rlpEncodeString( Hex2Raw( Keccak256("\x80") ) )
+                                                +String #rlpEncodeString( Hex2Raw( Keccak256("") ) )
+                                              , 192
+                                              )
+
+    syntax AccountData ::= AcctData ( nonce: Int, balance: Int, store: Map, code: ByteArray )
+ // -----------------------------------------------------------------------------------------
+
+    syntax String      ::= #rlpEncodeFullAccount( AccountData ) [function]
+ // ----------------------------------------------------------------------
+    rule  #rlpEncodeFullAccount( AcctData( NONCE, BAL, STORAGE, CODE ) )
+         => #rlpEncodeLength(         #rlpEncodeWord(NONCE)
+                              +String #rlpEncodeWord(BAL)
+                              +String #rlpEncodeString( Hex2Raw( Keccak256( #rlpEncodeMerkleTree( #storageRoot( STORAGE ) ) ) ) )
+                              +String #rlpEncodeString( Hex2Raw( Keccak256( #asString( CODE ) ) ) )
+                            , 192
+                            )
 
 endmodule
 ```
diff --git a/tests/web3/firefly_getStateRootAll.expected.json b/tests/web3/firefly_getStateRootAll.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":{"stateRoot":"0x62da78953c804219d3f2e14c92337806cf0604b57060b528ec480c4f89fdbe4e"}}]
diff --git a/tests/web3/firefly_getStateRootAll.in.json b/tests/web3/firefly_getStateRootAll.in.json
@@ -0,0 +1,17 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "nonce":"0x1",
+        "balance":"0x56bc75e2d63100000",
+        "code":"0x6080604052348015600f57600080fd5b5060868061001e6000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80636d4ce63c14602d575b600080fd5b6033604c565b6040805163ffffffff9092168252519081900360200190f35b602a9056fea265627a7a72315820c0bd34730815aaf15c03933af0d41b94653dfda48fd932e0bcd9c83bc61cd5fa64736f6c634300050b0032"
+    }]
+},
+{
+    "jsonrpc":"2.0",
+    "id":2,
+    "method":"firefly_getStateRoot",
+    "params":[]
+}]
diff --git a/tests/web3/firefly_getStateRootBalance.expected.json b/tests/web3/firefly_getStateRootBalance.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":{"stateRoot":"0x0e0fb05cc0c18ae82d7742186716ecf01555dc7736119aba5e9424123c56bc1c"}}]
diff --git a/tests/web3/firefly_getStateRootBalance.in.json b/tests/web3/firefly_getStateRootBalance.in.json
@@ -0,0 +1,15 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "balance":"0x56bc75e2d63100000"
+    }]
+},
+{
+    "jsonrpc":"2.0",
+    "id":2,
+    "method":"firefly_getStateRoot",
+    "params":[]
+}]
diff --git a/tests/web3/firefly_getStateRootCode.expected.json b/tests/web3/firefly_getStateRootCode.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":{"stateRoot":"0xf8b8aab7e98399674eb2f6cffe421220bed88b519cc17145724a453352df4343"}}]
diff --git a/tests/web3/firefly_getStateRootCode.in.json b/tests/web3/firefly_getStateRootCode.in.json
@@ -0,0 +1,15 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "code":"0x6080604052348015600f57600080fd5b5060868061001e6000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80636d4ce63c14602d575b600080fd5b6033604c565b6040805163ffffffff9092168252519081900360200190f35b602a9056fea265627a7a72315820c0bd34730815aaf15c03933af0d41b94653dfda48fd932e0bcd9c83bc61cd5fa64736f6c634300050b0032"
+    }]
+},
+{
+    "jsonrpc":"2.0",
+    "id":2,
+    "method":"firefly_getStateRoot",
+    "params":[]
+}]
diff --git a/tests/web3/firefly_getStateRootNonce.expected.json b/tests/web3/firefly_getStateRootNonce.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":{"stateRoot":"0xb62b878cd9003caa9f8e830bdf2ba6b68539dae38c4f51d7e5e5c7973b62a893"}}]
diff --git a/tests/web3/firefly_getStateRootNonce.in.json b/tests/web3/firefly_getStateRootNonce.in.json
@@ -0,0 +1,15 @@
+[{
+    "jsonrpc":"2.0",
+    "id":1,
+    "method":"firefly_addAccount",
+    "params":[{
+        "key":"0xcdeac0dd5ec7c04072af48f2a4451e102a80ca5bb441a7b4d72c176cea61866e",
+        "nonce":"0x1"
+    }]
+},
+{
+    "jsonrpc":"2.0",
+    "id":2,
+    "method":"firefly_getStateRoot",
+    "params":[]
+}]
diff --git a/web3.md b/web3.md
@@ -317,6 +317,8 @@ WEB3 JSON RPC
          <method> "eth_estimateGas" </method>
     rule <k> #runRPCCall => #firefly_getCoverageData ... </k>
          <method> "firefly_getCoverageData" </method>
+    rule <k> #runRPCCall => #firefly_getStateRoot ... </k>
+         <method> "firefly_getStateRoot" </method>
 
     rule <k> #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... </k> [owise]
 
@@ -1198,5 +1200,45 @@ Collecting Coverage Data
     syntax Int ::= #computePercentage ( Int, Int ) [function]
  // ---------------------------------------------------------
     rule #computePercentage (EXECUTED, TOTAL) => (100 *Int EXECUTED) /Int TOTAL
+```
+
+Helper Funcs
+------------
+
+```k
+    syntax AccountData ::= #getAcctData( Account ) [function]
+ // ---------------------------------------------------------
+    rule [[ #getAcctData( ACCT ) => AcctData(NONCE, BAL, STORAGE, CODE) ]]
+         <account>
+           <acctID>  ACCT    </acctID>
+           <nonce>   NONCE   </nonce>
+           <balance> BAL     </balance>
+           <storage> STORAGE </storage>
+           <code>    CODE    </code>
+           ...
+         </account>
+```
+
+State Root
+----------
+
+```k
+    syntax MerkleTree ::= "#stateRoot" [function]
+ // ---------------------------------------------
+    rule #stateRoot => MerkleUpdateMap( .MerkleTree, #precompiledContracts #activeAccounts )
+
+    syntax Map ::= "#activeAccounts"   [function]
+                 | #accountsMap( Set ) [function]
+ // ---------------------------------------------
+    rule [[ #activeAccounts => #accountsMap( ACCTS ) ]]
+         <activeAccounts> ACCTS </activeAccounts>
+
+    rule #accountsMap( .Set ) => .Map
+    rule #accountsMap( SetItem( ACCT:Int ) S ) => #parseByteStack( #unparseData( ACCT, 20 ) ) |-> #rlpEncodeFullAccount( #getAcctData( ACCT ) ) #accountsMap( S )
+
+    syntax KItem ::= "#firefly_getStateRoot"
+ // ----------------------------------------
+    rule <k> #firefly_getStateRoot => #sendResponse("result": { "stateRoot" : "0x" +String Keccak256( #rlpEncodeMerkleTree( #stateRoot ) ) } ) ... </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":{"stateRoot":"0x62da78953c804219d3f2e14c92337806cf0604b57060b528ec480c4f89fdbe4e"}}]