Skip to content

Commit b304508

Browse files
gtreptarv-jenkins
gtrepta
authored and
rv-jenkins
committed
storageRoot Implementation (#532)
* storageRoot * Fix #hashedLocation to always return a hash * Change header in documentation * Revert "Fix #hashedLocation to always return a hash" This reverts commit 4992c69. * Less hacky use of hashedLocation * New test for storageRoot * Add more test cases
1 parent 3cecbb6 commit b304508

File tree

3 files changed

+126
-0
lines changed

3 files changed

+126
-0
lines changed

‎Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -417,6 +417,7 @@ tests/%.parse: tests/%
417417
rm -rf $@-out
418418

419419
tests/specs/functional/%.prove: TEST_SYMBOLIC_BACKEND=haskell
420+
tests/specs/functional/storageRoot-spec.k.prove: TEST_SYMBOLIC_BACKEND=java
420421

421422
tests/%.prove: tests/%
422423
$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)

‎data.md

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1166,6 +1166,22 @@ Merkle Tree Aux Functions
11661166
rule #merkleExtensionSplitter( PATH, P1, TREE, P2, VALUE )
11671167
=> MerkleExtension( PATH, #merkleExtensionBrancher( MerkleUpdate( .MerkleBranch, P2, VALUE ), P1, TREE ) )
11681168
requires #sizeByteArray(P2) ==Int 0
1169+
```
1170+
1171+
Tree Root Helper Functions
1172+
--------------------------
1173+
1174+
### Storage Root
1175+
1176+
```k
1177+
syntax Map ::= #intMap2StorageMap( Map ) [function]
1178+
// ---------------------------------------------------
1179+
rule #intMap2StorageMap( .Map ) => .Map
1180+
rule #intMap2StorageMap( KEY |-> VAL M ) => #padToWidth( 32, #asByteStack( KEY ) ) |-> #rlpEncodeWord( VAL ) #intMap2StorageMap(M)
1181+
1182+
syntax MerkleTree ::= #storageRoot( Map ) [function]
1183+
// ----------------------------------------------------
1184+
rule #storageRoot( STORAGE ) => MerkleUpdateMap( .MerkleTree, #intMap2StorageMap( STORAGE ) )
11691185
11701186
endmodule
11711187
```

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

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
requires "evm.k"
2+
requires "edsl.k"
3+
4+
module VERIFICATION
5+
imports EVM
6+
imports EDSL
7+
8+
syntax StepSort ::= MerkleTree | String
9+
syntax KItem ::= runMerkle ( StepSort )
10+
| doneMerkle( StepSort )
11+
// ------------------------------------------
12+
rule runMerkle( T ) => doneMerkle( T )
13+
14+
endmodule
15+
16+
module STORAGEROOT-SPEC
17+
imports VERIFICATION
18+
19+
rule <k> runMerkle( #storageRoot( .Map ) )
20+
=> doneMerkle( .MerkleTree )
21+
</k>
22+
23+
// uint pos0;
24+
//
25+
// pos0 = 1234;
26+
rule <k> runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
27+
#hashedLocation( "Solidity", 0, .IntList ) |-> 1234
28+
)
29+
)
30+
)
31+
)
32+
=> doneMerkle( "6ff6cfba457bc662332201b53a8bda503e307197962f2c51e5e2dcc3809e19be" )
33+
</k>
34+
35+
// mapping (uint => uint) pos0;
36+
//
37+
// pos0[0] = 100;
38+
// pos0[1] = 200;
39+
rule <k> runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
40+
#hashedLocation( "Solidity", 0, 0 ) |-> 100
41+
#hashedLocation( "Solidity", 0, 1 ) |-> 200
42+
)
43+
)
44+
)
45+
)
46+
=> doneMerkle( "27093708a19995cf73ddd4b27049a7e33fb49e242bde6c1bffbb6596b67b8b3e" )
47+
</k>
48+
49+
// uint pos0;
50+
// mapping (uint => uint) pos1;
51+
//
52+
// pos0 = 600;
53+
// pos1[0] = 200;
54+
// pos1[5] = 24;
55+
rule <k> runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
56+
#hashedLocation( "Solidity", 0, .IntList ) |-> 600
57+
#hashedLocation( "Solidity", 1, 0 ) |-> 200
58+
#hashedLocation( "Solidity", 1, 5 ) |-> 24
59+
)
60+
)
61+
)
62+
)
63+
=> doneMerkle( "7df5d7b198240b49434b4e1dbff02fcb0649dd91650ae0fae191b2881cbb009e" )
64+
</k>
65+
66+
// mapping (uint => uint) pos0;
67+
// mapping (uint => uint) pos1;
68+
//
69+
// pos0[0] = 123;
70+
// pos0[1] = 456;
71+
// pos1[6] = 56;
72+
// pos1[9] = 333;
73+
rule <k> runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
74+
#hashedLocation( "Solidity", 0, 0 ) |-> 123
75+
#hashedLocation( "Solidity", 0, 1 ) |-> 456
76+
#hashedLocation( "Solidity", 1, 6 ) |-> 56
77+
#hashedLocation( "Solidity", 1, 9 ) |-> 333
78+
)
79+
)
80+
)
81+
)
82+
=> doneMerkle( "e3d130ca69a8d33ad2058d86ba26ec414f6e5639930041d6a266ee88b25ea835" )
83+
</k>
84+
85+
// uint pos0;
86+
// mapping (uint => uint) pos1;
87+
// uint pos2;
88+
// mapping (uint => mapping (uint => uint)) pos3;
89+
//
90+
// pos0 = 1234;
91+
// pos1[0] = 0;
92+
// pos1[1] = 1;
93+
// pos2 = 100;
94+
// pos3[0][0] = 42;
95+
// pos3[2][1] = 2019;
96+
rule <k> runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
97+
#hashedLocation( "Solidity", 0, .IntList ) |-> 1234
98+
#hashedLocation( "Solidity", 1, 0 ) |-> 0
99+
#hashedLocation( "Solidity", 1, 1 ) |-> 1
100+
#hashedLocation( "Solidity", 2, .IntList ) |-> 100
101+
#hashedLocation( "Solidity", 3, 0 0 ) |-> 42
102+
#hashedLocation( "Solidity", 3, 2 1 ) |-> 2019
103+
)
104+
)
105+
)
106+
)
107+
=> doneMerkle( "6786e17b1f185ba3b51ec15f28526a1d47d74052ca98c1b8edf7cdc6243eebba" )
108+
</k>
109+
endmodule

0 commit comments

Comments
 (0)