From 3cecbb6b8da0f55587d5549e20898794c35ca897 Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Tue, 29 Oct 2019 11:25:29 -0500
Subject: [PATCH] Merkle Tree bugfix + new function (#530)

* Add MerkleUpdateMap

* Fix nibbleize (nibble arrangement) and byteify (zero byte)

* Remove unnecessary rule
---
 data.md                              | 17 ++++++++++++++---
 tests/specs/functional/merkle-spec.k | 11 +++++++++++
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/data.md b/data.md
index 0c5aa82285..2cae8690e1 100644
--- a/data.md
+++ b/data.md
@@ -1073,6 +1073,16 @@ 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
 -------------------------
 
@@ -1080,13 +1090,14 @@ Merkle Tree Aux Functions
     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
index 8dff43200c..49acd096a9 100644
--- 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