Merkle Tree bugfix + new function (#530)

* Add MerkleUpdateMap * Fix nibbleize (nibble arrangement) and byteify (zero byte) * Remove unnecessary rule
runtimeverification · Oct 29, 2019 · 3cecbb6 · 3cecbb6
1 parent 9a1e580
commit 3cecbb6
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 3 deletions.
diff --git a/data.md b/data.md
@@ -1073,20 +1073,31 @@ Merkle Patricia Tree
       => #merkleBrancher ( M, BRANCHVALUE, PATH[0], PATH[1 .. #sizeByteArray(PATH) -Int 1], VALUE ) [owise]
 ```
 
+- `MerkleUpdateMap` Takes a mapping of `ByteArray |-> String` and generates a trie
+
+```k
+    syntax MerkleTree ::= MerkleUpdateMap( MerkleTree, Map ) [function]
+ // -------------------------------------------------------------------
+    rule MerkleUpdateMap( TREE, KEY |-> VALUE M ) => MerkleUpdateMap( MerkleUpdate( TREE, #nibbleize(KEY), VALUE ) , M )
+
+    rule MerkleUpdateMap( TREE, .Map ) => TREE
+```
+
 Merkle Tree Aux Functions
 -------------------------
 
 ```k
     syntax ByteArray ::= #nibbleize ( ByteArray ) [function]
                        | #byteify   ( ByteArray ) [function]
  // --------------------------------------------------------
-    rule #nibbleize ( B ) =>    #asByteStack ( ( B [ 0 ] /Int 16 ) *Int 256 +Int ( B [ 0 ] %Int 16 ) )[0 .. 2]
-                             ++ #nibbleize ( B[1 .. #sizeByteArray(B) -Int 1] )
+    rule #nibbleize ( B ) => (    #asByteStack ( ( B [ 0 ] /Int 16 ) *Int 256 )[0 .. 1]
+                               ++ ( #asByteStack ( B [ 0 ] %Int 16 )[0 .. 1] )
+                             ) ++ #nibbleize ( B[1 .. #sizeByteArray(B) -Int 1] )
       requires #sizeByteArray( B ) >Int 0
 
     rule #nibbleize ( _ ) => .ByteArray [owise]
 
-    rule #byteify ( B ) =>    #asByteStack ( B[0] *Int 16 +Int B[1] )
+    rule #byteify ( B ) =>    #asByteStack ( B[0] *Int 16 +Int B[1] )[0 .. 1]
                            ++ #byteify ( B[2 .. #sizeByteArray(B) -Int 2] )
       requires #sizeByteArray(B) >Int 0
 

diff --git a/tests/specs/functional/merkle-spec.k b/tests/specs/functional/merkle-spec.k
@@ -55,4 +55,15 @@ module MERKLE-SPEC
     rule <k> runMerkle ( Keccak256( #rlpEncodeMerkleTree( MerkleUpdate( MerkleUpdate( MerkleUpdate( MerkleUpdate( .MerkleTree, "do", "verb" ), "horse", "stallion" ), "doge", "coin" ), "dog", "puppy" ) ) ) )
           => doneMerkle( "5991bb8c6514148a29db676a14ac506cd2cd5775ace63c30a4fe457715e9ac84" ) </k>
 
+    rule <k> runMerkle( Keccak256( #rlpEncodeMerkleTree( MerkleUpdateMap( .MerkleTree,
+               #parseByteStack( "do" )    |-> "verb"
+               #parseByteStack( "dog" )   |-> "puppy"
+               #parseByteStack( "doge" )  |-> "coin"
+               #parseByteStack( "horse" ) |-> "stallion"
+                                                                        )
+                                                       )
+                                 )
+                      )
+          => doneMerkle( "5991bb8c6514148a29db676a14ac506cd2cd5775ace63c30a4fe457715e9ac84" )
+         </k>
 endmodule