Skip to content

Commit 9a1e580

Browse files
gtreptarv-jenkins
gtrepta
authored and
rv-jenkins
committed
Merkle Patricia Tries (#524)
* Merkle Tree structure * RLP Encoding of Merkle Trees * Add update logic for MerkleExtension * Add spec proof for Merkle Tree * Add update logic for .MerkleTree * Add update logic for MerkleLeaf * Add update logic for MerkleBranch * Fix change requests
1 parent e3ea413 commit 9a1e580

File tree

3 files changed

+261
-0
lines changed

3 files changed

+261
-0
lines changed

‎Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -416,6 +416,8 @@ tests/%.parse: tests/%
416416
$(CHECK) $@-expected $@-out
417417
rm -rf $@-out
418418

419+
tests/specs/functional/%.prove: TEST_SYMBOLIC_BACKEND=haskell
420+
419421
tests/%.prove: tests/%
420422
$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)
421423

‎data.md

Lines changed: 201 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -515,6 +515,10 @@ The local memory of execution is a byte-array (instead of a word-array).
515515
// --------------------------------------------------
516516
rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned)
517517
518+
syntax String ::= #asString ( ByteArray ) [function]
519+
// ----------------------------------------------------
520+
rule #asString(WS) => Bytes2String(WS)
521+
518522
syntax Account ::= #asAccount ( ByteArray ) [function]
519523
// ------------------------------------------------------
520524
rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0
@@ -560,6 +564,12 @@ The local memory of execution is a byte-array (instead of a word-array).
560564
rule #asInteger( W : .WordStack ) => W
561565
rule #asInteger( W0 : W1 : WS ) => #asInteger(((W0 *Int 256) +Int W1) : WS)
562566
567+
syntax String ::= #asString ( ByteArray ) [function]
568+
// ----------------------------------------------------
569+
rule #asString( .WordStack ) => ""
570+
rule #asString( W : .WordStack ) => chrChar( W )
571+
rule #asString( W0 : WS ) => chrChar( W0 ) +String #asString( WS )
572+
563573
syntax Account ::= #asAccount ( ByteArray ) [function]
564574
// ------------------------------------------------------
565575
rule #asAccount( .WordStack ) => .Account
@@ -914,6 +924,48 @@ Encoding
914924
rule #rlpEncodeLength(STR, OFFSET) => chrChar(lengthString(STR) +Int OFFSET) +String STR requires lengthString(STR) <Int 56
915925
rule #rlpEncodeLength(STR, OFFSET) => #rlpEncodeLength(STR, OFFSET, #unparseByteStack(#asByteStack(lengthString(STR)))) requires lengthString(STR) >=Int 56
916926
rule #rlpEncodeLength(STR, OFFSET, BL) => chrChar(lengthString(BL) +Int OFFSET +Int 55) +String BL +String STR
927+
928+
syntax String ::= #rlpEncodeMerkleTree ( MerkleTree ) [function]
929+
// ----------------------------------------------------------------
930+
rule #rlpEncodeMerkleTree ( .MerkleTree ) => "\x80"
931+
932+
rule #rlpEncodeMerkleTree ( MerkleLeaf ( PATH, VALUE ) )
933+
=> #rlpEncodeLength( #rlpEncodeString( #asString( #HPEncode( PATH, 1 ) ) )
934+
+String #rlpEncodeString( VALUE )
935+
, 192
936+
)
937+
938+
rule #rlpEncodeMerkleTree ( MerkleExtension ( PATH, TREE ) )
939+
=> #rlpEncodeLength( #rlpEncodeString( #asString( #HPEncode( PATH, 0 ) ) )
940+
+String #rlpMerkleH( #rlpEncodeMerkleTree( TREE ) )
941+
, 192
942+
)
943+
944+
rule #rlpEncodeMerkleTree ( MerkleBranch ( 0 |-> P0:MerkleTree 1 |-> P1:MerkleTree 2 |-> P2:MerkleTree 3 |-> P3:MerkleTree
945+
4 |-> P4:MerkleTree 5 |-> P5:MerkleTree 6 |-> P6:MerkleTree 7 |-> P7:MerkleTree
946+
8 |-> P8:MerkleTree 9 |-> P9:MerkleTree 10 |-> P10:MerkleTree 11 |-> P11:MerkleTree
947+
12 |-> P12:MerkleTree 13 |-> P13:MerkleTree 14 |-> P14:MerkleTree 15 |-> P15:MerkleTree
948+
, VALUE
949+
)
950+
)
951+
=> #rlpEncodeLength( #rlpMerkleH( #rlpEncodeMerkleTree( P0 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P1 ) )
952+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P2 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P3 ) )
953+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P4 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P5 ) )
954+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P6 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P7 ) )
955+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P8 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P9 ) )
956+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P10 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P11 ) )
957+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P12 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P13 ) )
958+
+String #rlpMerkleH( #rlpEncodeMerkleTree( P14 ) ) +String #rlpMerkleH( #rlpEncodeMerkleTree( P15 ) )
959+
+String #rlpEncodeString( VALUE )
960+
, 192
961+
)
962+
963+
syntax String ::= #rlpMerkleH ( String ) [function,klabel(MerkleRLPAux)]
964+
// ------------------------------------------------------------------------
965+
rule #rlpMerkleH ( X ) => #rlpEncodeString( Hex2Raw( Keccak256( X ) ) )
966+
requires lengthString( X ) >=Int 32
967+
968+
rule #rlpMerkleH ( X ) => X [owise]
917969
```
918970

919971
Decoding
@@ -955,5 +1007,154 @@ Decoding
9551007
rule #decodeLengthPrefixLength(#str, STR, START, B0) => #decodeLengthPrefixLength(#str, START, B0 -Int 128 -Int 56 +Int 1, #asWord(#parseByteStackRaw(substrString(STR, START +Int 1, START +Int 1 +Int (B0 -Int 128 -Int 56 +Int 1)))))
9561008
rule #decodeLengthPrefixLength(#list, STR, START, B0) => #decodeLengthPrefixLength(#list, START, B0 -Int 192 -Int 56 +Int 1, #asWord(#parseByteStackRaw(substrString(STR, START +Int 1, START +Int 1 +Int (B0 -Int 192 -Int 56 +Int 1)))))
9571009
rule #decodeLengthPrefixLength(TYPE, START, LL, L) => TYPE(L, START +Int 1 +Int LL)
1010+
```
1011+
1012+
Merkle Patricia Tree
1013+
====================
1014+
1015+
- Appendix C and D from the Ethereum Yellow Paper
1016+
- https://github.com/ethereum/wiki/wiki/Patricia-Tree
1017+
1018+
```k
1019+
syntax KItem ::= Int | MerkleTree // For testing purposes
1020+
1021+
syntax MerkleTree ::= MerkleBranch ( Map, String )
1022+
| MerkleExtension ( ByteArray, MerkleTree )
1023+
| MerkleLeaf ( ByteArray, String )
1024+
| ".MerkleTree"
1025+
| ".MerkleBranch" [function]
1026+
// -----------------------------------------------------------
1027+
rule .MerkleBranch
1028+
=> MerkleBranch ( 0 |-> .MerkleTree 1 |-> .MerkleTree 2 |-> .MerkleTree 3 |-> .MerkleTree
1029+
4 |-> .MerkleTree 5 |-> .MerkleTree 6 |-> .MerkleTree 7 |-> .MerkleTree
1030+
8 |-> .MerkleTree 9 |-> .MerkleTree 10 |-> .MerkleTree 11 |-> .MerkleTree
1031+
12 |-> .MerkleTree 13 |-> .MerkleTree 14 |-> .MerkleTree 15 |-> .MerkleTree
1032+
, ""
1033+
)
1034+
1035+
syntax MerkleTree ::= MerkleUpdate ( MerkleTree, String, String ) [function]
1036+
| MerkleUpdate ( MerkleTree, ByteArray, String ) [function,klabel(MerkleUpdateAux)]
1037+
// --------------------------------------------------------------------------------------------------------
1038+
rule MerkleUpdate ( TREE, S:String, VALUE ) => MerkleUpdate ( TREE, #nibbleize ( #parseByteStackRaw( S ) ), VALUE )
1039+
1040+
rule MerkleUpdate ( .MerkleTree, PATH:ByteArray, VALUE ) => MerkleLeaf ( PATH, VALUE )
1041+
1042+
rule MerkleUpdate ( MerkleLeaf ( LEAFPATH, _ ), PATH, VALUE )
1043+
=> MerkleLeaf( LEAFPATH, VALUE )
1044+
requires #asInteger( LEAFPATH ) ==Int #asInteger( PATH )
1045+
1046+
rule MerkleUpdate ( MerkleLeaf ( LEAFPATH, LEAFVALUE ), PATH, VALUE )
1047+
=> MerkleUpdate ( MerkleUpdate ( .MerkleBranch, LEAFPATH, LEAFVALUE ), PATH, VALUE )
1048+
requires #sizeByteArray( LEAFPATH ) >Int 0
1049+
andBool #sizeByteArray( PATH ) >Int 0
1050+
andBool LEAFPATH[0] =/=Int PATH[0]
1051+
1052+
rule MerkleUpdate ( MerkleLeaf ( LEAFPATH, LEAFVALUE ), PATH, VALUE )
1053+
=> #merkleExtensionBuilder( .ByteArray, LEAFPATH, LEAFVALUE, PATH, VALUE ) [owise]
1054+
1055+
rule MerkleUpdate ( MerkleExtension ( EXTPATH, EXTTREE ), PATH, VALUE )
1056+
=> MerkleExtension ( EXTPATH, MerkleUpdate ( EXTTREE, .ByteArray, VALUE ) )
1057+
requires #asInteger( EXTPATH ) ==Int #asInteger( PATH )
1058+
1059+
rule MerkleUpdate ( MerkleExtension ( EXTPATH, EXTTREE ), PATH, VALUE )
1060+
=> #merkleExtensionBrancher( MerkleUpdate( .MerkleBranch, PATH, VALUE ), EXTPATH, EXTTREE )
1061+
requires #sizeByteArray( EXTPATH ) >Int 0
1062+
andBool #sizeByteArray( PATH ) >Int 0
1063+
andBool EXTPATH[0] =/=Int PATH[0]
1064+
1065+
rule MerkleUpdate ( MerkleExtension ( EXTPATH, EXTTREE ), PATH, VALUE )
1066+
=> #merkleExtensionSplitter( .ByteArray, EXTPATH, EXTTREE, PATH, VALUE ) [owise]
1067+
1068+
rule MerkleUpdate ( MerkleBranch( M, _ ), PATH, VALUE )
1069+
=> MerkleBranch( M, VALUE )
1070+
requires #sizeByteArray( PATH ) ==Int 0
1071+
1072+
rule MerkleUpdate ( MerkleBranch( M, BRANCHVALUE ), PATH, VALUE )
1073+
=> #merkleBrancher ( M, BRANCHVALUE, PATH[0], PATH[1 .. #sizeByteArray(PATH) -Int 1], VALUE ) [owise]
1074+
```
1075+
1076+
Merkle Tree Aux Functions
1077+
-------------------------
1078+
1079+
```k
1080+
syntax ByteArray ::= #nibbleize ( ByteArray ) [function]
1081+
| #byteify ( ByteArray ) [function]
1082+
// --------------------------------------------------------
1083+
rule #nibbleize ( B ) => #asByteStack ( ( B [ 0 ] /Int 16 ) *Int 256 +Int ( B [ 0 ] %Int 16 ) )[0 .. 2]
1084+
++ #nibbleize ( B[1 .. #sizeByteArray(B) -Int 1] )
1085+
requires #sizeByteArray( B ) >Int 0
1086+
1087+
rule #nibbleize ( _ ) => .ByteArray [owise]
1088+
1089+
rule #byteify ( B ) => #asByteStack ( B[0] *Int 16 +Int B[1] )
1090+
++ #byteify ( B[2 .. #sizeByteArray(B) -Int 2] )
1091+
requires #sizeByteArray(B) >Int 0
1092+
1093+
rule #byteify ( _ ) => .ByteArray [owise]
1094+
1095+
syntax ByteArray ::= #HPEncode ( ByteArray, Int ) [function]
1096+
// ------------------------------------------------------------
1097+
rule #HPEncode ( X, T ) => #asByteStack ( ( HPEncodeAux(T) +Int 1 ) *Int 16 +Int X[0] ) ++ #byteify( X[1 .. #sizeByteArray(X) -Int 1] )
1098+
requires #sizeByteArray(X) %Int 2 =/=Int 0
1099+
1100+
rule #HPEncode ( X, T ) => #asByteStack ( HPEncodeAux(T) *Int 16 )[0 .. 1] ++ #byteify( X ) [owise]
1101+
1102+
syntax Int ::= HPEncodeAux ( Int ) [function]
1103+
// ---------------------------------------------
1104+
rule HPEncodeAux ( X ) => 0 requires X ==Int 0
1105+
rule HPEncodeAux ( _ ) => 2 [owise]
1106+
1107+
syntax MerkleTree ::= #merkleBrancher ( Map, String, Int, ByteArray, String ) [function]
1108+
// ----------------------------------------------------------------------------------------
1109+
rule #merkleBrancher ( X |-> TREE M, BRANCHVALUE, X, PATH, VALUE )
1110+
=> MerkleBranch( M[X <- MerkleUpdate( TREE, PATH, VALUE )], BRANCHVALUE )
1111+
1112+
syntax MerkleTree ::= #merkleExtensionBuilder( ByteArray, ByteArray, String, ByteArray, String ) [function]
1113+
// -----------------------------------------------------------------------------------------------------------
1114+
rule #merkleExtensionBuilder( PATH, P1, V1, P2, V2 )
1115+
=> #merkleExtensionBuilder( PATH ++ ( #asByteStack( P1[0] )[0 .. 1] )
1116+
, P1[1 .. #sizeByteArray(P1) -Int 1], V1
1117+
, P2[1 .. #sizeByteArray(P2) -Int 1], V2
1118+
)
1119+
[owise]
1120+
1121+
rule #merkleExtensionBuilder( PATH, P1, V1, P2, V2 )
1122+
=> MerkleExtension( PATH, MerkleUpdate( MerkleUpdate( .MerkleBranch, P1, V1 ), P2, V2 ) )
1123+
requires #sizeByteArray(P1) >Int 0
1124+
andBool #sizeByteArray(P2) >Int 0
1125+
andBool P1[0] =/=Int P2[0]
1126+
1127+
rule #merkleExtensionBuilder( PATH, P1, V1, P2, V2 )
1128+
=> MerkleExtension( PATH, MerkleUpdate( MerkleUpdate( .MerkleBranch, P1, V1 ), P2, V2 ) )
1129+
requires #sizeByteArray(P1) ==Int 0
1130+
orBool #sizeByteArray(P2) ==Int 0
1131+
1132+
syntax MerkleTree ::= #merkleExtensionBrancher ( MerkleTree, ByteArray, MerkleTree ) [function]
1133+
| #merkleExtensionSplitter ( ByteArray, ByteArray, MerkleTree, ByteArray, String ) [function]
1134+
// -----------------------------------------------------------------------------------------------------------------
1135+
rule #merkleExtensionBrancher( MerkleBranch(M, VALUE), PATH, EXTTREE )
1136+
=> MerkleBranch( M[PATH[0] <- MerkleExtension( PATH[1 .. #sizeByteArray(PATH) -Int 1], EXTTREE )], VALUE )
1137+
1138+
rule #merkleExtensionSplitter( PATH, P1, TREE, P2, VALUE )
1139+
=> #merkleExtensionSplitter( PATH ++ ( #asByteStack( P1[0] )[0 .. 1] )
1140+
, P1[1 .. #sizeByteArray(P1) -Int 1], TREE
1141+
, P2[1 .. #sizeByteArray(P2) -Int 1], VALUE
1142+
)
1143+
[owise]
1144+
1145+
rule #merkleExtensionSplitter( PATH, P1, TREE, P2, VALUE )
1146+
=> MerkleExtension( PATH, #merkleExtensionBrancher( MerkleUpdate( .MerkleBranch, P2, VALUE ), P1, TREE ) )
1147+
requires #sizeByteArray(P1) >Int 0
1148+
andBool #sizeByteArray(P2) >Int 0
1149+
andBool P1[0] =/=Int P2[0]
1150+
1151+
rule #merkleExtensionSplitter( PATH, P1, TREE, P2, VALUE )
1152+
=> MerkleExtension( PATH, MerkleUpdate( TREE, P2, VALUE ) )
1153+
requires #sizeByteArray(P1) ==Int 0
1154+
1155+
rule #merkleExtensionSplitter( PATH, P1, TREE, P2, VALUE )
1156+
=> MerkleExtension( PATH, #merkleExtensionBrancher( MerkleUpdate( .MerkleBranch, P2, VALUE ), P1, TREE ) )
1157+
requires #sizeByteArray(P2) ==Int 0
1158+
9581159
endmodule
9591160
```

‎tests/specs/functional/merkle-spec.k

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
requires "evm.k"
2+
3+
module VERIFICATION
4+
imports EVM
5+
6+
syntax StepSort ::= MerkleTree | String
7+
syntax KItem ::= runMerkle ( StepSort )
8+
| doneMerkle( StepSort )
9+
// ------------------------------------------
10+
rule runMerkle( T ) => doneMerkle( T )
11+
12+
endmodule
13+
14+
module MERKLE-SPEC
15+
imports VERIFICATION
16+
17+
rule <k> runMerkle ( MerkleUpdate( .MerkleTree, .WordStack, VALUE ) )
18+
=> doneMerkle( MerkleLeaf( .WordStack, VALUE ) ) </k>
19+
20+
// Update on MerkleLeaf
21+
rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( 6 : 7 : .WordStack, _ ), 6 : 7 : .WordStack, V ) )
22+
=> doneMerkle( MerkleLeaf ( 6 : 7 : .WordStack, V ) ) </k>
23+
24+
rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( 6 : 7 : .WordStack, _ ), 6 : 8 : .WordStack, _ ) )
25+
=> doneMerkle( MerkleExtension( 6 : .WordStack, _ ) ) </k>
26+
27+
rule <k> runMerkle ( MerkleUpdate( MerkleLeaf( 5 : .WordStack, _ ), 6 : .WordStack, _ ) )
28+
=> doneMerkle( MerkleBranch( _, _ ) ) </k>
29+
30+
// Update on MerkleExtension
31+
rule <k> runMerkle ( MerkleUpdate( MerkleExtension( 6 : .WordStack, .MerkleTree ), 6 : .WordStack, V ) )
32+
=> doneMerkle( MerkleExtension( 6 : .WordStack, MerkleLeaf( .WordStack, V ) ) ) </k>
33+
34+
rule <k> runMerkle ( MerkleUpdate( MerkleExtension( 7 : .WordStack, _ ), 6 : .WordStack, _ ) )
35+
=> doneMerkle( MerkleBranch( _, _ ) ) </k>
36+
37+
rule <k> runMerkle ( MerkleUpdate( MerkleExtension( 7 : 8 : .WordStack, _ ), 7 : 9 : .WordStack, _ ) )
38+
=> doneMerkle( MerkleExtension( 7 : .WordStack, MerkleBranch( _, _ ) ) ) </k>
39+
40+
// Update on MerkleBranch
41+
rule <k> runMerkle ( MerkleUpdate( MerkleBranch( M, _ ), .WordStack, V ) )
42+
=> doneMerkle( MerkleBranch( M, V ) ) </k>
43+
44+
rule <k> runMerkle ( .MerkleBranch )
45+
=> doneMerkle( MerkleBranch ( 0 |-> .MerkleTree 1 |-> .MerkleTree 2 |-> .MerkleTree 3 |-> .MerkleTree
46+
4 |-> .MerkleTree 5 |-> .MerkleTree 6 |-> .MerkleTree 7 |-> .MerkleTree
47+
8 |-> .MerkleTree 9 |-> .MerkleTree 10 |-> .MerkleTree 11 |-> .MerkleTree
48+
12 |-> .MerkleTree 13 |-> .MerkleTree 14 |-> .MerkleTree 15 |-> .MerkleTree
49+
, ""
50+
)
51+
)
52+
</k>
53+
54+
// Concrete Test
55+
rule <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( MerkleUpdate( MerkleUpdate( MerkleUpdate( .MerkleTree, "do", "verb" ), "horse", "stallion" ), "doge", "coin" ), "dog", "puppy" ) ) ) )
56+
=> doneMerkle( "5991bb8c6514148a29db676a14ac506cd2cd5775ace63c30a4fe457715e9ac84" ) </k>
57+
58+
endmodule

0 commit comments

Comments
 (0)