From b3045082e67435e74ed8dd6d349166a02b6c490c Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Thu, 31 Oct 2019 15:13:57 -0500
Subject: [PATCH] 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 4992c69c968bda8e760c94227d809c5bbbc07d3b.
* Less hacky use of hashedLocation
* New test for storageRoot
* Add more test cases
---
Makefile | 1 +
data.md | 16 ++++
tests/specs/functional/storageRoot-spec.k | 109 ++++++++++++++++++++++
3 files changed, 126 insertions(+)
create mode 100644 tests/specs/functional/storageRoot-spec.k
diff --git a/Makefile b/Makefile
index 6250a93556..be77859f75 100644
--- a/Makefile
+++ b/Makefile
@@ -417,6 +417,7 @@ tests/%.parse: tests/%
rm -rf $@-out
tests/specs/functional/%.prove: TEST_SYMBOLIC_BACKEND=haskell
+tests/specs/functional/storageRoot-spec.k.prove: TEST_SYMBOLIC_BACKEND=java
tests/%.prove: tests/%
$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)
diff --git a/data.md b/data.md
index 2cae8690e1..6dce771c62 100644
--- a/data.md
+++ b/data.md
@@ -1166,6 +1166,22 @@ Merkle Tree Aux Functions
rule #merkleExtensionSplitter( PATH, P1, TREE, P2, VALUE )
=> MerkleExtension( PATH, #merkleExtensionBrancher( MerkleUpdate( .MerkleBranch, P2, VALUE ), P1, TREE ) )
requires #sizeByteArray(P2) ==Int 0
+```
+
+Tree Root Helper Functions
+--------------------------
+
+### Storage Root
+
+```k
+ syntax Map ::= #intMap2StorageMap( Map ) [function]
+ // ---------------------------------------------------
+ rule #intMap2StorageMap( .Map ) => .Map
+ rule #intMap2StorageMap( KEY |-> VAL M ) => #padToWidth( 32, #asByteStack( KEY ) ) |-> #rlpEncodeWord( VAL ) #intMap2StorageMap(M)
+
+ syntax MerkleTree ::= #storageRoot( Map ) [function]
+ // ----------------------------------------------------
+ rule #storageRoot( STORAGE ) => MerkleUpdateMap( .MerkleTree, #intMap2StorageMap( STORAGE ) )
endmodule
```
diff --git a/tests/specs/functional/storageRoot-spec.k b/tests/specs/functional/storageRoot-spec.k
new file mode 100644
index 0000000000..f5a413d19f
--- /dev/null
+++ b/tests/specs/functional/storageRoot-spec.k
@@ -0,0 +1,109 @@
+requires "evm.k"
+requires "edsl.k"
+
+module VERIFICATION
+ imports EVM
+ imports EDSL
+
+ syntax StepSort ::= MerkleTree | String
+ syntax KItem ::= runMerkle ( StepSort )
+ | doneMerkle( StepSort )
+ // ------------------------------------------
+ rule runMerkle( T ) => doneMerkle( T )
+
+endmodule
+
+module STORAGEROOT-SPEC
+ imports VERIFICATION
+
+ rule runMerkle( #storageRoot( .Map ) )
+ => doneMerkle( .MerkleTree )
+
+
+ // uint pos0;
+ //
+ // pos0 = 1234;
+ rule runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
+ #hashedLocation( "Solidity", 0, .IntList ) |-> 1234
+ )
+ )
+ )
+ )
+ => doneMerkle( "6ff6cfba457bc662332201b53a8bda503e307197962f2c51e5e2dcc3809e19be" )
+
+
+ // mapping (uint => uint) pos0;
+ //
+ // pos0[0] = 100;
+ // pos0[1] = 200;
+ rule runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
+ #hashedLocation( "Solidity", 0, 0 ) |-> 100
+ #hashedLocation( "Solidity", 0, 1 ) |-> 200
+ )
+ )
+ )
+ )
+ => doneMerkle( "27093708a19995cf73ddd4b27049a7e33fb49e242bde6c1bffbb6596b67b8b3e" )
+
+
+ // uint pos0;
+ // mapping (uint => uint) pos1;
+ //
+ // pos0 = 600;
+ // pos1[0] = 200;
+ // pos1[5] = 24;
+ rule runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
+ #hashedLocation( "Solidity", 0, .IntList ) |-> 600
+ #hashedLocation( "Solidity", 1, 0 ) |-> 200
+ #hashedLocation( "Solidity", 1, 5 ) |-> 24
+ )
+ )
+ )
+ )
+ => doneMerkle( "7df5d7b198240b49434b4e1dbff02fcb0649dd91650ae0fae191b2881cbb009e" )
+
+
+ // mapping (uint => uint) pos0;
+ // mapping (uint => uint) pos1;
+ //
+ // pos0[0] = 123;
+ // pos0[1] = 456;
+ // pos1[6] = 56;
+ // pos1[9] = 333;
+ rule runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
+ #hashedLocation( "Solidity", 0, 0 ) |-> 123
+ #hashedLocation( "Solidity", 0, 1 ) |-> 456
+ #hashedLocation( "Solidity", 1, 6 ) |-> 56
+ #hashedLocation( "Solidity", 1, 9 ) |-> 333
+ )
+ )
+ )
+ )
+ => doneMerkle( "e3d130ca69a8d33ad2058d86ba26ec414f6e5639930041d6a266ee88b25ea835" )
+
+
+ // uint pos0;
+ // mapping (uint => uint) pos1;
+ // uint pos2;
+ // mapping (uint => mapping (uint => uint)) pos3;
+ //
+ // pos0 = 1234;
+ // pos1[0] = 0;
+ // pos1[1] = 1;
+ // pos2 = 100;
+ // pos3[0][0] = 42;
+ // pos3[2][1] = 2019;
+ rule runMerkle( Keccak256( #rlpEncodeMerkleTree( #storageRoot(
+ #hashedLocation( "Solidity", 0, .IntList ) |-> 1234
+ #hashedLocation( "Solidity", 1, 0 ) |-> 0
+ #hashedLocation( "Solidity", 1, 1 ) |-> 1
+ #hashedLocation( "Solidity", 2, .IntList ) |-> 100
+ #hashedLocation( "Solidity", 3, 0 0 ) |-> 42
+ #hashedLocation( "Solidity", 3, 2 1 ) |-> 2019
+ )
+ )
+ )
+ )
+ => doneMerkle( "6786e17b1f185ba3b51ec15f28526a1d47d74052ca98c1b8edf7cdc6243eebba" )
+
+endmodule