@@ -321,6 +321,8 @@ WEB3 JSON RPC
321
321
<method> "firefly_getStateRoot" </method>
322
322
rule <k> #runRPCCall => #firefly_getTxRoot ... </k>
323
323
<method> "firefly_getTxRoot" </method>
324
+ rule <k> #runRPCCall => #firefly_getReceiptsRoot ... </k>
325
+ <method> "firefly_getReceiptsRoot" </method>
324
326
325
327
rule <k> #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... </k> [owise]
326
328
@@ -1222,6 +1224,51 @@ Helper Funcs
1222
1224
<sigS> S </sigS>
1223
1225
<sigV> V </sigV>
1224
1226
</message>
1227
+
1228
+ syntax String ::= #rlpEncodeReceipt( Int ) [function]
1229
+ | #rlpEncodeReceiptAux( String ) [function]
1230
+ // -----------------------------------------------------------
1231
+ rule #rlpEncodeReceipt( I ) => #rlpEncodeReceiptAux( "0x" +String #hashSignedTx( I ) )
1232
+ rule [[ #rlpEncodeReceiptAux( TXHASH ) =>
1233
+ #rlpEncodeLength( #rlpEncodeWord( STATUS )
1234
+ +String #rlpEncodeWord( CGAS )
1235
+ +String #rlpEncodeString( #asString( BLOOM ) )
1236
+ +String #rlpEncodeLogs( LOGS )
1237
+ , 192
1238
+ )
1239
+ ]]
1240
+ <txReceipt>
1241
+ <txHash> TXHASH </txHash>
1242
+ <txCumulativeGas> CGAS </txCumulativeGas>
1243
+ <logSet> LOGS </logSet>
1244
+ <bloomFilter> BLOOM </bloomFilter>
1245
+ <txStatus> STATUS </txStatus>
1246
+ </txReceipt>
1247
+
1248
+ syntax String ::= #rlpEncodeLogs ( List ) [function]
1249
+ | #rlpEncodeLogsAux( List ) [function]
1250
+ // ------------------------------------------------------
1251
+ rule #rlpEncodeLogs( .List ) => "\xc0"
1252
+ rule #rlpEncodeLogs( LOGS ) => #rlpEncodeLength( #rlpEncodeLogsAux( LOGS ), 192 )
1253
+ requires LOGS =/=K .List
1254
+
1255
+ rule #rlpEncodeLogsAux( .List ) => ""
1256
+ rule #rlpEncodeLogsAux( ListItem({ ACCT | TOPICS | DATA }) LOGS )
1257
+ => #rlpEncodeLength( #rlpEncodeBytes( ACCT, 20 )
1258
+ +String #rlpEncodeTopics( TOPICS )
1259
+ +String #rlpEncodeString( #asString( DATA ) )
1260
+ , 192 )
1261
+ +String #rlpEncodeLogsAux( LOGS )
1262
+
1263
+ syntax String ::= #rlpEncodeTopics ( List ) [function]
1264
+ | #rlpEncodeTopicsAux( List ) [function]
1265
+ // --------------------------------------------------------
1266
+ rule #rlpEncodeTopics( .List ) => "\xc0"
1267
+ rule #rlpEncodeTopics( TOPICS ) => #rlpEncodeLength( #rlpEncodeTopicsAux( TOPICS ), 192 )
1268
+ requires TOPICS =/=K .List
1269
+
1270
+ rule #rlpEncodeTopicsAux( .List ) => ""
1271
+ rule #rlpEncodeTopicsAux( ListItem( X:Int ) TOPICS ) => #rlpEncodeWord( X ) +String #rlpEncodeTopicsAux( TOPICS )
1225
1272
```
1226
1273
1227
1274
State Root
@@ -1267,6 +1314,29 @@ Transactions Root
1267
1314
syntax KItem ::= "#firefly_getTxRoot"
1268
1315
// -------------------------------------
1269
1316
rule <k> #firefly_getTxRoot => #sendResponse("result": { "transactionsRoot" : "0x" +String Keccak256( #rlpEncodeMerkleTree( #transactionsRoot ) ) } ) ... </k>
1317
+ ```
1318
+
1319
+ Receipts Root
1320
+ -------------
1321
+
1322
+ ``` k
1323
+ syntax MerkleTree ::= "#receiptsRoot" [function]
1324
+ // ------------------------------------------------
1325
+ rule #receiptsRoot => MerkleUpdateMap( .MerkleTree, #receiptsMap )
1326
+
1327
+ syntax Map ::= "#receiptsMap" [function]
1328
+ | #receiptsMapAux( Int ) [function]
1329
+ // ------------------------------------------------
1330
+ rule #receiptsMap => #receiptsMapAux( 0 )
1331
+
1332
+ rule #receiptsMapAux( _ ) => .Map [owise]
1333
+ rule [[ #receiptsMapAux( I ) => #parseByteStackRaw( #rlpEncodeWord( I ) )[0 .. 1] |-> #rlpEncodeReceipt( { TXLIST[ I ] }:>Int ) #receiptsMapAux( I +Int 1 ) ]]
1334
+ <txOrder> TXLIST </txOrder>
1335
+ requires size(TXLIST) >Int I
1336
+
1337
+ syntax KItem ::= "#firefly_getReceiptsRoot"
1338
+ // -------------------------------------------
1339
+ rule <k> #firefly_getReceiptsRoot => #sendResponse("result": { "receiptsRoot" : "0x" +String Keccak256( #rlpEncodeMerkleTree( #receiptsRoot ) ) } ) ... </k>
1270
1340
1271
1341
endmodule
1272
1342
```
0 commit comments