From 031a2f37fa6fd1f72b0b437f88373d1ae1bb993d Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@runtimeverification.com>
Date: Tue, 22 Aug 2023 19:42:49 +0300
Subject: [PATCH] Update data structures; split the config for #writeToStorage

---
 data/list-bytes.k             |  19 +++---
 data/map-bytes-to-bytes.k     | 109 +++++++++++++++++-----------------
 data/map-int-to-bytes.k       |  76 ++++++++++++------------
 elrond-config.md              |  18 +++---
 vmhooks/baseOps.md            |   2 +-
 vmhooks/manBufOps.md          |   2 +-
 vmhooks/managedConversions.md |   2 +-
 7 files changed, 116 insertions(+), 112 deletions(-)

diff --git a/data/list-bytes.k b/data/list-bytes.k
index eac64f7e..79b2ae26 100644
--- a/data/list-bytes.k
+++ b/data/list-bytes.k
@@ -1,11 +1,10 @@
-requires "bytes-type.k"
+require "bytes-type.k"
 
 module LIST-BYTES
   imports private INT-SYNTAX
   imports private BASIC-K
-  
   imports BYTES-TYPE
-  
+
   syntax Bytes
 
   syntax ListBytes [hook(LIST.List)]
@@ -26,7 +25,7 @@ module LIST-BYTES
   syntax WrappedBytes ::= ListBytes "[" Int "]"
           [ function, hook(LIST.get), klabel(ListBytes:get), symbol ]
   syntax ListBytes ::= ListBytes "[" index: Int "<-" value: WrappedBytes "]"
-          [function, hook(LIST.update), klabel(ListBytes:set)]
+          [function, hook(LIST.update), symbol, klabel(ListBytes:set)]
   syntax ListBytes ::= makeListBytes(length: Int, value: WrappedBytes)
           [function, hook(LIST.make)]
   syntax ListBytes ::= updateList(dest: ListBytes, index: Int, src: ListBytes)
@@ -36,27 +35,26 @@ module LIST-BYTES
   syntax ListBytes ::= range(ListBytes, fromFront: Int, fromBack: Int)
           [function, hook(LIST.range), klabel(ListBytes:range), symbol]
   syntax Bool ::= WrappedBytes "in" ListBytes
-          [function, total, hook(LIST.in), klabel(_inListBytes_)]
+          [function, total, hook(LIST.in), symbol, klabel(_inListBytes_)]
   syntax Int ::= size(ListBytes)
-          [function, total, hook(LIST.size), klabel (sizeListBytes), smtlib(smt_seq_len)]
+          [function, total, hook(LIST.size), symbol, klabel (sizeListBytes), smtlib(smt_seq_len)]
 endmodule
 
 module LIST-BYTES-EXTENSIONS
   imports BOOL
   imports INT
   imports LIST-BYTES
-  imports BYTES-TYPE
 
   syntax WrappedBytes ::= ListBytes "[" Int "]" "orDefault" WrappedBytes
           [ function, total, klabel(ListBytes:getOrDefault), symbol ]
 
   syntax Bytes ::= ListBytes "{{" Int "}}"
-                 [function, klabel(ListBytes:primitiveLookup)]
+                 [function, symbol, klabel(ListBytes:primitiveLookup)]
 // -----------------------------------------------------------
   rule L:ListBytes {{ I:Int }} => unwrap( L[ I ] )
   
   syntax Bytes ::= ListBytes "{{" Int "}}" "orDefault" Bytes
-                 [ function, total, klabel(ListBytes:primitiveLookupOrDefault) ]
+                 [ function, total, symbol, klabel(ListBytes:primitiveLookupOrDefault) ]
 // -----------------------------------------------------------------------------
   rule L:ListBytes {{ I:Int }} orDefault Value:Bytes
       => unwrap( L [I] orDefault wrap(Value) )
@@ -78,7 +76,8 @@ module LIST-BYTES-EXTENSIONS
     requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
     [simplification]
 
-  syntax ListBytes ::= ListItemWrap( Bytes )    [function, total, klabel(ListBytesItemWrap)]
+  syntax ListBytes ::= ListItemWrap( Bytes )
+      [function, total, symbol, klabel(ListBytesItemWrap)]
   rule ListItemWrap( B:Bytes ) => ListItem(wrap(B))
 
 endmodule
diff --git a/data/map-bytes-to-bytes.k b/data/map-bytes-to-bytes.k
index 7a508965..6e5d6538 100644
--- a/data/map-bytes-to-bytes.k
+++ b/data/map-bytes-to-bytes.k
@@ -6,11 +6,12 @@ module MAP-BYTES-TO-BYTES
   imports private BOOL-SYNTAX
   imports private INT-SYNTAX
   imports private LIST-BYTES
+  imports private LIST-BYTES
   // imports private LIST
   // imports private SET-BYTES
   imports private SET
   imports BYTES-TYPE
-  // imports BYTES-TYPE
+  imports BYTES-TYPE
 
   syntax Bytes
   syntax Bytes
@@ -109,7 +110,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-CONCRETE [concrete]
                  [function, total, klabel(MapBytesToBytes:primitiveInKeys), symbol]
 
   rule (M:MapBytesToBytes {{ Key:Bytes }})
-      => unwrap( M[ wrap(Key) ] )
+      => (unwrap( M[wrap(Key)] ))
   rule M:MapBytesToBytes {{ Key:Bytes }} orDefault Value:Bytes
       => unwrap( M[wrap(Key)] orDefault wrap(Value) )
   rule M:MapBytesToBytes {{ Key:Bytes <- Value:Bytes }}
@@ -141,27 +142,27 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
   // Definitions
   // -----------
 
-  rule (Key Bytes2Bytes|-> V:Bytes M:MapBytesToBytes)
+  rule (wrap(Key) Bytes2Bytes|-> V:WrappedBytes M:MapBytesToBytes)
           {{ Key:Bytes }}
-      => V
+      => unwrap( V )
       ensures notBool Key in_keys {{ M }}
 
-  rule (Key Bytes2Bytes|-> V:Bytes M:MapBytesToBytes)
+  rule (wrap(Key) Bytes2Bytes|-> V:WrappedBytes M:MapBytesToBytes)
           {{ Key:Bytes }} orDefault _:Bytes
-      => V
+      => unwrap( V )
       ensures notBool Key in_keys {{ M }}
   rule M:MapBytesToBytes {{ Key:Bytes }} orDefault V:Bytes
       => V
       requires notBool Key in_keys {{ M }}
 
-  rule (Key Bytes2Bytes|-> _:Bytes M:MapBytesToBytes)
+  rule (wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes)
           {{ Key:Bytes <- Value:Bytes }}
-      => (Key Bytes2Bytes|-> Value) M
+      => (wrap(Key) Bytes2Bytes|-> wrap(Value)) M
   rule M:MapBytesToBytes {{ Key:Bytes <- Value:Bytes }}
-      => (Key Bytes2Bytes|-> Value) M
+      => (wrap(Key) Bytes2Bytes|-> wrap(Value)) M
       requires notBool Key in_keys {{ M }}
 
-  rule (Key Bytes2Bytes|-> _:Bytes M:MapBytesToBytes)
+  rule (wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes)
           {{ Key:Bytes <- undef }}
       => M
       ensures notBool Key in_keys {{ M }}
@@ -170,7 +171,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
       requires notBool Key in_keys {{ M }}
 
   rule Key:Bytes in_keys
-          {{Key Bytes2Bytes|-> _:Bytes M:MapBytesToBytes}}
+          {{wrap(Key) Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes}}
       => true
       ensures notBool Key in_keys {{ M }}
   rule _Key:Bytes in_keys {{ .MapBytesToBytes }}
@@ -180,62 +181,62 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
   // O(n^2) or something like that, where n is the number of explicit keys
   // in the map.
   rule Key:Bytes in_keys
-          {{Key2:Bytes Bytes2Bytes|-> _:Bytes M:MapBytesToBytes}}
+          {{Key2:WrappedBytes Bytes2Bytes|-> _:WrappedBytes M:MapBytesToBytes}}
       => Key in_keys {{ M }}
-      requires Key =/=K Key2
+      requires Key =/=K unwrap( Key2 )
       ensures notBool Key2 in_keys (M)
       [simplification]
 
   // Translation rules
-  rule M:MapBytesToBytes[ wrap(Key) ]
-      => M{{Key}}
+  rule M:MapBytesToBytes[Key:WrappedBytes]
+      => wrap(M{{unwrap( Key )}})
       [simplification, symbolic(M)]
-  rule M:MapBytesToBytes[ wrap(Key) ]
-      => M{{Key}}
+  rule M:MapBytesToBytes[Key:WrappedBytes]
+      => wrap(M{{unwrap( Key )}})
       [simplification, symbolic(Key)]
   rule M:MapBytesToBytes{{Key}}
-      => M[wrap(Key)]
+      => unwrap( M[wrap(Key)] )
       [simplification, concrete]
 
-  rule M:MapBytesToBytes [ wrap(Key) ] orDefault wrap(Value)
-      => M {{ Key }} orDefault Value
+  rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
+      => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
       [simplification, symbolic(M)]
-  rule M:MapBytesToBytes [ wrap(Key) ] orDefault wrap(Value)
-      => M {{ Key }} orDefault Value
+  rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
+      => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
       [simplification, symbolic(Key)]
-  rule M:MapBytesToBytes [ wrap(Key) ] orDefault wrap(Value)
-      => M {{ Key }} orDefault Value
+  rule M:MapBytesToBytes [ Key:WrappedBytes ] orDefault Value:WrappedBytes
+      => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
       [simplification, symbolic(Value)]
   rule M:MapBytesToBytes{{Key}} orDefault Value
-      => M[wrap(Key)] orDefault Value
+      => unwrap( M[wrap(Key)] orDefault wrap(Value) )
       [simplification, concrete]
 
-  rule M:MapBytesToBytes[wrap(Key) <- wrap(Value)]
-      => M {{ Key <- Value }}
+  rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
+      => M {{ unwrap( Key ) <- unwrap( Value ) }}
       [simplification, symbolic(M)]
-  rule M:MapBytesToBytes[wrap(Key) <- wrap(Value)]
-      => M {{ Key <- Value }}
+  rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
+      => M {{ unwrap( Key ) <- unwrap( Value ) }}
       [simplification, symbolic(Key)]
-  rule M:MapBytesToBytes[wrap(Key) <- wrap(Value)]
-      => M {{ Key <- Value }}
+  rule M:MapBytesToBytes[Key:WrappedBytes <- Value:WrappedBytes]
+      => M {{ unwrap( Key ) <- unwrap( Value ) }}
       [simplification, symbolic(Value)]
   rule M:MapBytesToBytes{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ]
       [simplification, concrete]
 
-  rule M:MapBytesToBytes[wrap(Key) <- undef]
-      => M {{ Key <- undef }}
+  rule M:MapBytesToBytes[Key:WrappedBytes <- undef]
+      => M {{ unwrap( Key ) <- undef }}
       [simplification, symbolic(M)]
-  rule M:MapBytesToBytes[wrap(Key) <- undef]
-      => M {{ Key <- undef }}
+  rule M:MapBytesToBytes[Key:WrappedBytes <- undef]
+      => M {{ unwrap( Key ) <- undef }}
       [simplification, symbolic(Key)]
   rule M:MapBytesToBytes{{Key <- undef}} => M[wrap(Key) <- undef]
       [simplification, concrete]
 
-  rule wrap(Key) in_keys (M:MapBytesToBytes)
-      => Key in_keys {{M}}
+  rule Key:WrappedBytes in_keys (M:MapBytesToBytes)
+      => unwrap( Key ) in_keys {{M}}
       [simplification, symbolic(M)]
-  rule wrap(Key) in_keys (M:MapBytesToBytes)
-      => Key in_keys {{M}}
+  rule Key:WrappedBytes in_keys (M:MapBytesToBytes)
+      => unwrap( Key ) in_keys {{M}}
       [simplification, symbolic(Key)]
   rule Key in_keys {{M:MapBytesToBytes}} => wrap(Key) in_keys(M)
       [simplification, concrete]
@@ -253,16 +254,16 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
   rule M:MapBytesToBytes {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification]
   rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- V2 }}
       => (K1 Bytes2Bytes|-> V1 (M {{ K2 <- V2 }}))
-      requires K1 =/=K K2
+      requires unwrap( K1 ) =/=K K2
       [simplification]
 
   rule (K1 Bytes2Bytes|-> V1 M:MapBytesToBytes) {{ K2 <- undef }}
       => (K1 Bytes2Bytes|-> V1 (M {{ K2 <- undef }}))
-      requires K1 =/=K K2
+      requires unwrap( K1 ) =/=K K2
       [simplification]
 
   rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} => M {{K2}}
-      requires K1 =/=K K2
+      requires unwrap( K1 ) =/=K K2
       ensures notBool (K1 in_keys(M))
       [simplification]
   rule (_MAP:MapBytesToBytes {{ K  <-  V1 }}) {{ K }}  => V1 [simplification]
@@ -272,7 +273,7 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
 
   rule (K1 Bytes2Bytes|-> _V M:MapBytesToBytes) {{ K2 }} orDefault D
       => M {{K2}} orDefault D
-      requires K1 =/=K K2
+      requires unwrap( K1 ) =/=K K2
       ensures notBool (K1 in_keys(M))
       [simplification]
   rule (_MAP:MapBytesToBytes {{ K  <-  V1 }}) {{ K }} orDefault _ => V1 [simplification]
@@ -292,19 +293,19 @@ module MAP-BYTES-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
       [simplification]
 
   rule K1 in_keys {{ (K2 Bytes2Bytes|-> V) M:MapBytesToBytes }}
-      => K1 ==K K2 orBool K1 in_keys {{ M }}
+      => K1 ==K unwrap( K2 ) orBool K1 in_keys {{ M }}
     requires definedMapElementConcat(K2, V, M)
     [simplification(100)]
 
 
   rule {false #Equals @Key in_keys{{ Key' Bytes2Bytes|-> Val @M:MapBytesToBytes }}}
       =>  #Ceil(@Key) #And #Ceil(Key' Bytes2Bytes|-> Val @M)
-          #And #Not({ @Key #Equals Key' })
+          #And #Not({ @Key #Equals unwrap( Key' ) })
           #And {false #Equals @Key in_keys{{@M}}}
       [simplification]
   rule {@Key in_keys{{Key' Bytes2Bytes|-> Val @M:MapBytesToBytes}} #Equals false}
       =>  #Ceil(@Key) #And #Ceil(Key' Bytes2Bytes|-> Val @M)
-          #And #Not({@Key #Equals Key' })
+          #And #Not({@Key #Equals unwrap( Key' ) })
           #And {@Key in_keys{{@M}} #Equals false}
       [simplification]
 
@@ -315,8 +316,8 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
   imports private K-EQUAL
   imports private BOOL
 
-  syntax Bool ::= definedMapElementConcat(Bytes, Bytes, MapBytesToBytes)  [function, total]
-  rule definedMapElementConcat(K, _V, M:MapBytesToBytes) => notBool wrap(K) in_keys(M)
+  syntax Bool ::= definedMapElementConcat(WrappedBytes, WrappedBytes, MapBytesToBytes)  [function, total]
+  rule definedMapElementConcat(K, _V, M:MapBytesToBytes) => notBool K in_keys(M)
 
   rule #Ceil(@M:MapBytesToBytes [@K:WrappedBytes])
       => {(@K in_keys(@M)) #Equals true}
@@ -379,18 +380,18 @@ module MAP-BYTES-TO-BYTES-KORE-SYMBOLIC
       requires K1 =/=K K2
       [simplification]
 
-  rule wrap(K) in_keys((wrap(K) Bytes2Bytes|-> wrap(V)) M:MapBytesToBytes)
+  rule K in_keys((K Bytes2Bytes|-> V) M:MapBytesToBytes)
       => true
     requires definedMapElementConcat(K, V, M)
     [simplification(50)]
-  rule wrap(K1) in_keys((wrap(K2) Bytes2Bytes|-> wrap(V)) M:MapBytesToBytes)
-      => wrap(K1) in_keys(M)
+  rule K1 in_keys((K2 Bytes2Bytes|-> V) M:MapBytesToBytes)
+      => K1 in_keys(M)
     requires true
         andBool definedMapElementConcat(K2, V, M)
         andBool K1 =/=K K2
     [simplification(50)]
-  rule wrap(K1) in_keys((wrap(K2) Bytes2Bytes|-> wrap(V)) M:MapBytesToBytes)
-      => wrap(K1) ==K wrap(K2) orBool wrap(K1) in_keys(M)
+  rule K1 in_keys((K2 Bytes2Bytes|-> V) M:MapBytesToBytes)
+      => K1 ==K K2 orBool K1 in_keys(M)
     requires definedMapElementConcat(K2, V, M)
     [simplification(100)]
 
@@ -414,7 +415,7 @@ module MAP-BYTES-TO-BYTES-CURLY-BRACE
   imports private K-EQUAL-SYNTAX
   imports MAP-BYTES-TO-BYTES
 
-  syntax MapBytesToBytes ::= MapBytesToBytes "{" key:Bytes "<-" value:Bytes "}"
+  syntax MapBytesToBytes ::= MapBytesToBytes "{" key:WrappedBytes "<-" value:WrappedBytes "}"
       [function, total, symbol, klabel(MapBytesToBytes:curly_update)]
   rule M:MapBytesToBytes{Key <- Value} => M (Key Bytes2Bytes|-> Value)
     requires notBool Key in_keys(M)
diff --git a/data/map-int-to-bytes.k b/data/map-int-to-bytes.k
index bc79d82b..ee638517 100644
--- a/data/map-int-to-bytes.k
+++ b/data/map-int-to-bytes.k
@@ -1,6 +1,6 @@
 
 require "int-type.k"
-// require "bytes-type.k"
+require "bytes-type.k"
 
 module MAP-INT-TO-BYTES
   imports private BOOL-SYNTAX
@@ -11,7 +11,7 @@ module MAP-INT-TO-BYTES
   // imports private SET-INT
   imports private SET
   imports INT-TYPE
-  // imports BYTES-TYPE
+  imports BYTES-TYPE
 
   syntax Int
   syntax Bytes
@@ -26,7 +26,7 @@ module MAP-INT-TO-BYTES
          [ function, total, hook(MAP.unit),
            klabel(.MapIntToBytes), symbol, latex(\dotCt{MapIntToBytes})
          ]
-  syntax MapIntToBytes ::= WrappedInt "Int2Bytes|->" Bytes
+  syntax MapIntToBytes ::= WrappedInt "Int2Bytes|->" WrappedBytes
          [ function, total, hook(MAP.element),
            klabel(_Int2Bytes|->_), symbol,
            latex({#1}\mapsto{#2}), injective
@@ -34,13 +34,13 @@ module MAP-INT-TO-BYTES
 
   syntax priorities _Int2Bytes|->_ > _MapIntToBytes_ .MapIntToBytes
   syntax non-assoc _Int2Bytes|->_
-  syntax Bytes ::= MapIntToBytes "[" WrappedInt "]"
+  syntax WrappedBytes ::= MapIntToBytes "[" WrappedInt "]"
                  [function, hook(MAP.lookup), klabel(MapIntToBytes:lookup), symbol]
-  syntax Bytes ::= MapIntToBytes "[" WrappedInt "]" "orDefault" Bytes
+  syntax WrappedBytes ::= MapIntToBytes "[" WrappedInt "]" "orDefault" WrappedBytes
                  [ function, total, hook(MAP.lookupOrDefault),
                    klabel(MapIntToBytes:lookupOrDefault), symbol
                  ]
-  syntax MapIntToBytes ::= MapIntToBytes "[" key: WrappedInt "<-" value: Bytes "]"
+  syntax MapIntToBytes ::= MapIntToBytes "[" key: WrappedInt "<-" value: WrappedBytes "]"
                  [ function, total, klabel(MapIntToBytes:update), symbol,
                    hook(MAP.update), prefer
                  ]
@@ -110,11 +110,11 @@ module MAP-INT-TO-BYTES-PRIMITIVE-CONCRETE [concrete]
                  [function, total, klabel(MapIntToBytes:primitiveInKeys), symbol]
 
   rule (M:MapIntToBytes {{ Key:Int }})
-      => (M[wrap(Key)])
+      => (unwrap( M[wrap(Key)] ))
   rule M:MapIntToBytes {{ Key:Int }} orDefault Value:Bytes
-      => M[wrap(Key)] orDefault Value
+      => unwrap( M[wrap(Key)] orDefault wrap(Value) )
   rule M:MapIntToBytes {{ Key:Int <- Value:Bytes }}
-      => M[wrap(Key) <- Value]
+      => M[wrap(Key) <- wrap(Value)]
   rule M:MapIntToBytes {{ Key:Int <- undef }}
       => M[wrap(Key) <- undef]
   rule Key:Int in_keys {{ M:MapIntToBytes }} => wrap(Key) in_keys(M)
@@ -142,27 +142,27 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
   // Definitions
   // -----------
 
-  rule (wrap(Key) Int2Bytes|-> V:Bytes M:MapIntToBytes)
+  rule (wrap(Key) Int2Bytes|-> V:WrappedBytes M:MapIntToBytes)
           {{ Key:Int }}
-      => V
+      => unwrap( V )
       ensures notBool Key in_keys {{ M }}
 
-  rule (wrap(Key) Int2Bytes|-> V:Bytes M:MapIntToBytes)
+  rule (wrap(Key) Int2Bytes|-> V:WrappedBytes M:MapIntToBytes)
           {{ Key:Int }} orDefault _:Bytes
-      => V
+      => unwrap( V )
       ensures notBool Key in_keys {{ M }}
   rule M:MapIntToBytes {{ Key:Int }} orDefault V:Bytes
       => V
       requires notBool Key in_keys {{ M }}
 
-  rule (wrap(Key) Int2Bytes|-> _:Bytes M:MapIntToBytes)
+  rule (wrap(Key) Int2Bytes|-> _:WrappedBytes M:MapIntToBytes)
           {{ Key:Int <- Value:Bytes }}
-      => (wrap(Key) Int2Bytes|-> Value) M
+      => (wrap(Key) Int2Bytes|-> wrap(Value)) M
   rule M:MapIntToBytes {{ Key:Int <- Value:Bytes }}
-      => (wrap(Key) Int2Bytes|-> Value) M
+      => (wrap(Key) Int2Bytes|-> wrap(Value)) M
       requires notBool Key in_keys {{ M }}
 
-  rule (wrap(Key) Int2Bytes|-> _:Bytes M:MapIntToBytes)
+  rule (wrap(Key) Int2Bytes|-> _:WrappedBytes M:MapIntToBytes)
           {{ Key:Int <- undef }}
       => M
       ensures notBool Key in_keys {{ M }}
@@ -171,7 +171,7 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
       requires notBool Key in_keys {{ M }}
 
   rule Key:Int in_keys
-          {{wrap(Key) Int2Bytes|-> _:Bytes M:MapIntToBytes}}
+          {{wrap(Key) Int2Bytes|-> _:WrappedBytes M:MapIntToBytes}}
       => true
       ensures notBool Key in_keys {{ M }}
   rule _Key:Int in_keys {{ .MapIntToBytes }}
@@ -181,7 +181,7 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
   // O(n^2) or something like that, where n is the number of explicit keys
   // in the map.
   rule Key:Int in_keys
-          {{Key2:WrappedInt Int2Bytes|-> _:Bytes M:MapIntToBytes}}
+          {{Key2:WrappedInt Int2Bytes|-> _:WrappedBytes M:MapIntToBytes}}
       => Key in_keys {{ M }}
       requires Key =/=K unwrap( Key2 )
       ensures notBool Key2 in_keys (M)
@@ -189,38 +189,38 @@ module MAP-INT-TO-BYTES-PRIMITIVE-SYMBOLIC  [symbolic]
 
   // Translation rules
   rule M:MapIntToBytes[Key:WrappedInt]
-      => M{{unwrap( Key )}}
+      => wrap(M{{unwrap( Key )}})
       [simplification, symbolic(M)]
   rule M:MapIntToBytes[Key:WrappedInt]
-      => M{{unwrap( Key )}}
+      => wrap(M{{unwrap( Key )}})
       [simplification, symbolic(Key)]
   rule M:MapIntToBytes{{Key}}
-      => M[wrap(Key)]
+      => unwrap( M[wrap(Key)] )
       [simplification, concrete]
 
-  rule M:MapIntToBytes [ Key:WrappedInt ] orDefault Value:Bytes
-      => M {{ unwrap( Key ) }} orDefault Value
+  rule M:MapIntToBytes [ Key:WrappedInt ] orDefault Value:WrappedBytes
+      => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
       [simplification, symbolic(M)]
-  rule M:MapIntToBytes [ Key:WrappedInt ] orDefault Value:Bytes
-      => M {{ unwrap( Key ) }} orDefault Value
+  rule M:MapIntToBytes [ Key:WrappedInt ] orDefault Value:WrappedBytes
+      => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
       [simplification, symbolic(Key)]
-  rule M:MapIntToBytes [ Key:WrappedInt ] orDefault Value:Bytes
-      => M {{ unwrap( Key ) }} orDefault Value
+  rule M:MapIntToBytes [ Key:WrappedInt ] orDefault Value:WrappedBytes
+      => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
       [simplification, symbolic(Value)]
   rule M:MapIntToBytes{{Key}} orDefault Value
-      => M[wrap(Key)] orDefault Value
+      => unwrap( M[wrap(Key)] orDefault wrap(Value) )
       [simplification, concrete]
 
-  rule M:MapIntToBytes[Key:WrappedInt <- Value:Bytes]
-      => M {{ unwrap( Key ) <- Value }}
+  rule M:MapIntToBytes[Key:WrappedInt <- Value:WrappedBytes]
+      => M {{ unwrap( Key ) <- unwrap( Value ) }}
       [simplification, symbolic(M)]
-  rule M:MapIntToBytes[Key:WrappedInt <- Value:Bytes]
-      => M {{ unwrap( Key ) <- Value }}
+  rule M:MapIntToBytes[Key:WrappedInt <- Value:WrappedBytes]
+      => M {{ unwrap( Key ) <- unwrap( Value ) }}
       [simplification, symbolic(Key)]
-  rule M:MapIntToBytes[Key:WrappedInt <- Value:Bytes]
-      => M {{ unwrap( Key ) <- Value }}
+  rule M:MapIntToBytes[Key:WrappedInt <- Value:WrappedBytes]
+      => M {{ unwrap( Key ) <- unwrap( Value ) }}
       [simplification, symbolic(Value)]
-  rule M:MapIntToBytes{{Key <- Value}} => M[wrap(Key) <- Value ]
+  rule M:MapIntToBytes{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ]
       [simplification, concrete]
 
   rule M:MapIntToBytes[Key:WrappedInt <- undef]
@@ -316,7 +316,7 @@ module MAP-INT-TO-BYTES-KORE-SYMBOLIC
   imports private K-EQUAL
   imports private BOOL
 
-  syntax Bool ::= definedMapElementConcat(WrappedInt, Bytes, MapIntToBytes)  [function, total]
+  syntax Bool ::= definedMapElementConcat(WrappedInt, WrappedBytes, MapIntToBytes)  [function, total]
   rule definedMapElementConcat(K, _V, M:MapIntToBytes) => notBool K in_keys(M)
 
   rule #Ceil(@M:MapIntToBytes [@K:WrappedInt])
@@ -415,7 +415,7 @@ module MAP-INT-TO-BYTES-CURLY-BRACE
   imports private K-EQUAL-SYNTAX
   imports MAP-INT-TO-BYTES
 
-  syntax MapIntToBytes ::= MapIntToBytes "{" key:WrappedInt "<-" value:Bytes "}"
+  syntax MapIntToBytes ::= MapIntToBytes "{" key:WrappedInt "<-" value:WrappedBytes "}"
       [function, total, symbol, klabel(MapIntToBytes:curly_update)]
   rule M:MapIntToBytes{Key <- Value} => M (Key Int2Bytes|-> Value)
     requires notBool Key in_keys(M)
diff --git a/elrond-config.md b/elrond-config.md
index a3a3ad28..bf50b00e 100644
--- a/elrond-config.md
+++ b/elrond-config.md
@@ -170,9 +170,18 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
          <callee> CALLEE </callee>
          <account>
            <address> CALLEE </address>
-           <storage> STORAGE => #updateStorage(STORAGE, KEY, VALUE) </storage>
+           <storage> STORAGE => STORAGE{{KEY <- undef}} </storage>
            ...
          </account>
+         requires VALUE ==K .Bytes
+    rule <instrs> #writeToStorage(KEY, VALUE) => i32.const #storageStatus(STORAGE, KEY, VALUE) ... </instrs>
+         <callee> CALLEE </callee>
+         <account>
+           <address> CALLEE </address>
+           <storage> STORAGE => STORAGE{{KEY <- VALUE}} </storage>
+           ...
+         </account>
+         requires VALUE =/=K .Bytes
 
     rule [writeToStorage-unknown-addr]:
         <instrs> #writeToStorage(_, _) => #throwException(ExecutionFailed, "writeToStorage: unknown account address") ... </instrs>
@@ -212,11 +221,6 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
         // <bytesStack> ADDR : _ : _ </bytesStack>
       [owise]
 
-    syntax MapBytesToBytes ::= #updateStorage ( MapBytesToBytes , key : Bytes , val : Bytes ) [function, total]
- // ----------------------------------------------------------------------------------------
-    rule #updateStorage(STOR, KEY, VAL) => STOR {{KEY <- undef}} requires VAL  ==K .Bytes
-    rule #updateStorage(STOR, KEY, VAL) => STOR {{KEY <- VAL  }} requires VAL =/=K .Bytes
-
     syntax Bytes ::= #lookupStorage ( MapBytesToBytes , key: Bytes ) [function, total]
  // ---------------------------------------------------------------
     rule #lookupStorage(STORAGE, KEY) => STORAGE{{KEY}} orDefault .Bytes
@@ -243,7 +247,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
 ### Integer Operation
 
 ```k
-    syntax Int ::= #cmpInt ( Int , Int ) [function, total]
+    syntax Int ::= #cmpInt ( Int , Int ) [function, total, symbol, klabel(cmpInt), smtlib(cmpInt)]
  // -----------------------------------------------------------
     rule #cmpInt(I1, I2) => -1 requires I1  <Int I2
     rule #cmpInt(I1, I2) =>  1 requires I1  >Int I2
diff --git a/vmhooks/baseOps.md b/vmhooks/baseOps.md
index d6c81a9b..63f74743 100644
--- a/vmhooks/baseOps.md
+++ b/vmhooks/baseOps.md
@@ -367,7 +367,7 @@ module BASEOPS
                  ...
         </instrs>
         <locals> 0 |-> <i32> ID_IDX </locals>
-        <bufferHeap> ... wrap(ID_IDX) Int2Bytes|-> TokId ... </bufferHeap>
+        <bufferHeap> ... wrap(ID_IDX) Int2Bytes|-> wrap(TokId) ... </bufferHeap>
 
   // TODO check arguments and handle errors if any
   // TODO handle Callee is not a contract
diff --git a/vmhooks/manBufOps.md b/vmhooks/manBufOps.md
index 7cb54ded..80994d1e 100644
--- a/vmhooks/manBufOps.md
+++ b/vmhooks/manBufOps.md
@@ -25,7 +25,7 @@ module MANBUFOPS
     syntax BytesResult ::= getBuffer(Int)                                   [function, total]
  // ---------------------------------------------------------------------------------------------
     rule [[ getBuffer(BUFFER_IDX) => {Bs}:>BytesResult ]]
-      <bufferHeap> ... wrap(BUFFER_IDX) Int2Bytes|-> Bs:Bytes ... </bufferHeap>
+      <bufferHeap> ... wrap(BUFFER_IDX) Int2Bytes|-> wrap(Bs:Bytes) ... </bufferHeap>
 
     rule getBuffer(_) => {Err("no managed buffer under the given handle")}:>BytesResult [owise]
 
diff --git a/vmhooks/managedConversions.md b/vmhooks/managedConversions.md
index b7b4c2da..1b3169c0 100644
--- a/vmhooks/managedConversions.md
+++ b/vmhooks/managedConversions.md
@@ -80,7 +80,7 @@ module MANAGEDCONVERSIONS
     syntax ListBytesResult ::= readManagedVecOfManagedBuffers(Int)                     [function, total]
  // ----------------------------------------------------------------------------------------------------
     rule [[ readManagedVecOfManagedBuffers(BUFFER_IDX) => chunks2buffers(VecBs) ]]
-      <bufferHeap> ... wrap(BUFFER_IDX) Int2Bytes|-> VecBs:Bytes ... </bufferHeap>
+      <bufferHeap> ... wrap(BUFFER_IDX) Int2Bytes|-> wrap(VecBs:Bytes) ... </bufferHeap>
     rule readManagedVecOfManagedBuffers(_) => Err("no managed buffer under the given handle")
       [owise]