Implement Map (#15)

* Implement `Map` * Set Version: 0.1.9 * add comments * map.md - reformat sections and comments * data.md - document ScVal * Set Version: 0.1.10 * ensure consistent order in `allocObject-map` --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jul 27, 2024 · d02f5f7 · d02f5f7
1 parent 8a6cf9a
commit d02f5f7
Show file tree

Hide file tree

Showing 9 changed files with 706 additions and 49 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.9
+0.1.10
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "ksoroban"
-version = "0.1.9"
+version = "0.1.10"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md
@@ -26,7 +26,7 @@ module CONFIG
           <hostObjects> .List </hostObjects> // List of ScVals
           <callStack> .List </callStack>
           <interimStates> .List </interimStates>
-        </host>  
+        </host>
 
         <contracts>
           <contract multiplicity="*" type="Map">
@@ -46,7 +46,7 @@ module CONFIG
       </soroban>
 
     syntax HostStack ::= List{HostStackVal, ":"}  [symbol(hostStackList)]
-    syntax HostStackVal ::= ScVal | HostVal | Bytes
+    syntax HostStackVal ::= ScVal | HostVal | Bytes | List
 
 
     syntax InternalCmd ::= #callResult(ValStack, List)   [symbol(#callResult)]
@@ -81,7 +81,7 @@ module CONFIG-OPERATIONS
 
 ## Call State
 
-The `<callStack>` cell stores a list of previous contract execution states. 
+The `<callStack>` cell stores a list of previous contract execution states.
 These internal commands manages the call stack when calling and returning from a contract.
 
 ```k
@@ -156,13 +156,13 @@ These internal commands manages the call stack when calling and returning from a
 
 ### Creating host objects
 
-If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object 
-and pushes a `HostVal` onto the `<hostStack>` that points to the newly created object. 
-If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content 
+If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object
+and pushes a `HostVal` onto the `<hostStack>` that points to the newly created object.
+If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content
 but only pushes a single `HostVal` for the entire container onto the stack.
 If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly equivalent to `SCV`.
- 
-```k 
+
+```k
     syntax InternalCmd ::= allocObject(ScVal)             [symbol(allocObject)]
  // ---------------------------------------------------------------------------
     rule [allocObject-small]:
@@ -177,12 +177,40 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
          ~> allocObjectVecAux
             ...
         </k>
-    
-    syntax InternalCmd ::= "allocObjectVecAux"
- // ------------------------------------------
+
+    // recursively allocate map values.
+    rule [allocObject-map]:
+        <k> allocObject(ScMap(ITEMS))
+        // Using `lookupMany` with `keys_list` instead of `values`
+        // to ensure the order of values matches the order of keys.
+         => allocObjects(lookupMany(ITEMS, keys_list(ITEMS), 0)) 
+         ~> allocObjectMapAux(keys_list(ITEMS))
+            ...
+        </k>
+
+    syntax Map ::= mapFromLists(List, List)      [function, total, symbol(mapFromLists)]
+ // --------------------------------------------------------------------------------
+    rule mapFromLists(ListItem(KEY) KEYS, ListItem(VAL) VALS)
+      => mapFromLists(KEYS, VALS) [ KEY <- VAL]
+
+    rule mapFromLists(_, _) => .Map
+      [owise]
+
+    syntax InternalCmd ::= "allocObjectVecAux"    [symbol(allocObjectVecAux)]
+ // -------------------------------------------------------------------------
     rule [allocObjectVecAux]:
         <k> allocObjectVecAux => addObject(ScVec(V)) ... </k>
-        <hostStack> ScVec(V) : S => S </hostStack>
+        <hostStack> V : S => S </hostStack>
+
+    syntax InternalCmd ::= allocObjectMapAux(List)    [symbol(allocObjectMapAux)]
+ // -------------------------------------------------------------------------
+    rule [allocObjectMapAux]:
+        <k> allocObjectMapAux(KEYS)
+         => addObject(ScMap(mapFromLists(KEYS, VALS)))
+            ...
+        </k>
+        <hostStack> VALS : S => S </hostStack>
+      requires size(KEYS) ==Int size(VALS)
 
     rule [allocObject]:
         <k> allocObject(SCV) => addObject(SCV) ... </k>
@@ -204,31 +232,37 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
 
     syntax InternalCmd ::= allocObjects       (List)       [symbol(allocObjects)]
                          | allocObjectsAux    (List)       [symbol(allocObjectsAux)]
-                         | allocObjectsCollect(Int)        [symbol(allocObjectsCollect)]
  // ---------------------------------------------------------------------------
     rule [allocObjects]:
-        <k> allocObjects(L) => allocObjectsAux(L) ~> allocObjectsCollect(size(L))  ... </k>
+        <k> allocObjects(L) => allocObjectsAux(L) ~> collectStackObjects(size(L))  ... </k>
 
     rule [allocObjectsAux-empty]:
         <k> allocObjectsAux(.List) => .K ... </k>
 
     rule [allocObjectsAux]:
-        <k> allocObjectsAux(ListItem(SCV:ScVal) L) 
+        <k> allocObjectsAux(ListItem(SCV:ScVal) L)
          => allocObjectsAux(L)
          ~> allocObject(SCV)
             ...
         </k>
 
     rule [allocObjectsAux-HostVal]:
-        <k> allocObjectsAux(ListItem(HV:HostVal) L) 
+        <k> allocObjectsAux(ListItem(HV:HostVal) L)
          => allocObjectsAux(L)
          ~> pushStack(HV)
             ...
         </k>
 
-    rule [allocObjectsCollect]:
-        <k> allocObjectsCollect(LENGTH) => .K ... </k> 
-        <hostStack> STACK => ScVec(take(LENGTH, STACK)) : drop(LENGTH, STACK) </hostStack>
+    // Collect stack values into a List
+    syntax InternalCmd ::= collectStackObjects(Int)        [symbol(collectStackObjects)]
+ // ---------------------------------------------------------------------------------------
+    rule [collectStackObjects]:
+        <k> collectStackObjects(LENGTH) => .K ... </k>
+        <hostStack> STACK => take(LENGTH, STACK) : drop(LENGTH, STACK) </hostStack>
+
+    rule [collectStackObjects-instr]:
+        <instrs> collectStackObjects(LENGTH) => .K ... </instrs>
+        <hostStack> STACK => take(LENGTH, STACK) : drop(LENGTH, STACK) </hostStack>
 
 ```
 
@@ -248,7 +282,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
        andBool getIndex(VAL) <Int size(OBJS)
 
     rule [loadObject-rel]:
-        <instrs> loadObject(VAL) 
+        <instrs> loadObject(VAL)
               => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0))
                  ...
         </instrs>
@@ -264,7 +298,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
       requires notBool isObject(VAL)
        andBool fromSmallValid(VAL)
 
-    
+
 ```
 
 ### Auxiliary functions
@@ -274,27 +308,37 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
  // -------------------------------------------------------------------------------------
     rule drop(N, _ : S) => drop(N -Int 1, S)                requires N >Int 0
     rule drop(_,     S) => S                                [owise]
-    
+
     syntax List ::= take(Int, HostStack)        [function, total, symbol(HostStack:take)]
  // -------------------------------------------------------------------------------------
     rule take(N, X : S) => ListItem(X) take(N -Int 1, S)    requires N >Int 0
     rule take(_,     _) => .List                            [owise]
 ```
 
+- `lookupMany`: Retrieve values for multiple keys from a map. Return the specified default value for missing keys.
+
+```k
+    syntax List ::= lookupMany(Map, List, KItem)   [function, total]
+ // ----------------------------------------------------------------
+    rule lookupMany(M, ListItem(A) REST, D) => ListItem(M [ A ] orDefault D) lookupMany(M, REST, D)
+    rule lookupMany(_, _,                _) => .List
+        [owise]
+```
+
 ## Call result handling
 
 ```k
     rule [callResult-empty]:
         <k> #callResult(.ValStack, _RELS) => .K ... </k>
-    
+
     rule [callResult]:
         <k> #callResult(<i64> I : SS, RELS)
          => #callResult(SS, RELS)
          ~> pushStack(HostVal2ScVal(HostVal(I), OBJS, RELS))
             ...
         </k>
         <hostObjects> OBJS </hostObjects>
-    
+
     // Convert HostVals to ScVal recursively
     syntax ScVal ::= HostVal2ScVal(HostVal, objs: List, rels: List)      [function, total, symbol(HostVal2ScVal)]
  // -------------------------------------------------------------------------------------------------------------------
@@ -318,19 +362,23 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
     syntax ScVal ::= HostVal2ScValRec(ScVal, objs: List, rels: List)     [function, total, symbol(HostVal2ScValRec)]
  // -------------------------------------------------------------------------------------------------------------------
     rule HostVal2ScValRec(ScVec(VEC), OBJS, RELS) => ScVec(HostVal2ScValMany(VEC, OBJS, RELS))
+
+    rule HostVal2ScValRec(ScMap(M), OBJS, RELS)
+      => ScMap(mapFromLists( keys_list(M), HostVal2ScValMany(values(M), OBJS, RELS)) )
+
     rule HostVal2ScValRec(SCV, _OBJS, _RELS)      => SCV                                        [owise]
-    
+
     syntax List  ::= HostVal2ScValMany(List, objs: List, rels: List)     [function, total, symbol(HostVal2ScValMany)]
  // -------------------------------------------------------------------------------------------------------------------
     rule HostVal2ScValMany(ListItem(V:HostVal) REST, OBJS, RELS)
       => ListItem(HostVal2ScVal(V, OBJS, RELS))    HostVal2ScValMany(REST, OBJS, RELS)
-    
+
     rule HostVal2ScValMany(ListItem(V:ScVal)   REST, OBJS, RELS)
       => ListItem(HostVal2ScValRec(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS)
-    
+
     rule HostVal2ScValMany(_, _, _)
       => .List     [owise]
-    
+
 ```
 
 ```k

diff --git a/src/ksoroban/kdist/soroban-semantics/data.md b/src/ksoroban/kdist/soroban-semantics/data.md
@@ -1,3 +1,4 @@
+# Host Data Types
 
 [Documentation - Host Value Type](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type)
 
@@ -15,21 +16,47 @@ module HOST-OBJECT-SYNTAX
 
 [Documentation: ScVal](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#scval)
 
-`ScVal` is a union of various datatypes used in the context of smart contracts for passing values to and from contracts and
-storing data on the host side. 
+`ScVal` is a union of various datatypes used in the context of smart contracts for passing values to and from contracts
+and storing data on the host side.
+It combines elements from Stellar XDR’s `ScVal` and the Soroban Rust environment’s `HostObject` type (_Stellar XDR_ is
+the data format storing and communicating blockchain data).
 
+* [Stellar XDR - `ScVal`](https://github.com/stellar/stellar-xdr/blob/78ef9860777bd53e75a8ce8b978131cade26b321/Stellar-contract.x#L214)
+* [Soroban Environment - `HostObject`](https://github.com/stellar/rs-soroban-env/blob/00ddd2714e757d0005bfc98798f05aa209f283bf/soroban-env-host/src/host_object.rs#L22)
+
+There are notable differences between XDR’s `ScVal` and Rust’s `HostObject`:
+
+* Data Representation: XDR `ScVal` and Rust `HostObject` differ in their data representation and storage.
+  XDR’s `ScVal` is recursive on container types such as map and vector, meaning it stores `ScVal`s as both keys and
+  values within vectors and maps, allowing for nested data structures. In contrast, `HostObject` uses `HostVal` in
+  container types, which requires resolving the corresponding host objects when accessing these values. 
+* Containers: XDR uses sorted vectors of key-value pairs for maps with binary search for lookups. The Rust environment
+  also uses a sorted vector but stores `HostVal` within these containers. Our semantics, however, use `Map` instead for
+  efficient lookup and simpler implementation.
+
+In our semantic implementation, `ScVal` is utilized to represent both XDR `ScVal` and Rust `HostObject`, adapting to
+various contexts:
+
+* Inside the Host:
+  * `ScVec`: Represented as a `List` of `HostVal`
+  * `ScMap`: Represented as a `Map` from `ScVal` to `HostVal`.
+    Using `ScVal` as keys allows for more efficient lookups because it avoids the additional layer of indirection that
+    would be required if `HostVal` were used.
+* Outside the Host:
+  * `ScVec`: Represented as a `List` of `ScVal`.
+  * `ScVec`: Represented as a `Map` from `ScVal` to `ScVal`.
 
 ```k
-    syntax ScVal 
+    syntax ScVal
      ::= SCBool(Bool)                              [symbol(SCVal:Bool)]
         | "Void"                                   [symbol(SCVal:Void)]
         | U32(Int)                                 [symbol(SCVal:U32)]
         | I32(Int)                                 [symbol(SCVal:I32)]
         | U64(Int)                                 [symbol(SCVal:U64)]
         | I64(Int)                                 [symbol(SCVal:I64)]
         | U128(Int)                                [symbol(SCVal:U128)]
-        | ScVec(List)                              [symbol(SCVal:Vec)]
-        | ScMap(Map)                               [symbol(SCVal:Map)]
+        | ScVec(List)                              [symbol(SCVal:Vec)]      // List<HostVal>
+        | ScMap(Map)                               [symbol(SCVal:Map)]      // Map<ScVal, HostVal>
         | ScAddress(Address)                       [symbol(SCVal:Address)]
         | Symbol(String)                           [symbol(SCVal:Symbol)]
 
@@ -78,11 +105,11 @@ module HOST-OBJECT
     rule getBody(HostVal(I))  => I >>Int 8
 
     syntax Bool ::= isObject(HostVal)                   [function, total, symbol(isObject)]
-                  | isObjectTag(Int)                [function, total, symbol(isObjectTag)]
+                  | isObjectTag(Int)                    [function, total, symbol(isObjectTag)]
                   | isRelativeObjectHandle(HostVal)     [function, total, symbol(isRelativeObjectHandle)]
  // --------------------------------------------------------------------------------
     rule isObject(V)               => isObjectTag(getTag(V))
-    rule isObjectTag(TAG)          => 64 <=Int TAG andBool TAG <=Int 77  
+    rule isObjectTag(TAG)          => 64 <=Int TAG andBool TAG <=Int 77
     rule isRelativeObjectHandle(V) => getMajor(V) &Int 1 ==Int 0
 
     syntax Int ::= indexToHandle(Int, Bool)       [function, total, symbol(indexToHandle)]
@@ -93,7 +120,7 @@ module HOST-OBJECT
     syntax Int ::= getIndex(HostVal)   [function, total, symbol(getIndex)]
  // ----------------------------------------------------------------------------
     rule getIndex(V) => getMajor(V) >>Int 1
-    
+
     syntax HostVal ::= fromHandleAndTag(Int, Int)                [function, total, symbol(fromHandleAndTag)]
                      | fromMajorMinorAndTag(Int, Int, Int)       [function, total, symbol(fromMajorMinorAndTag)]
                      | fromBodyAndTag(Int, Int)                  [function, total, symbol(fromBodyAndTag)]
@@ -112,7 +139,7 @@ module HOST-OBJECT
     rule getTag(SCBool(true))  => 0
     rule getTag(SCBool(false)) => 1
     rule getTag(Void)          => 2
-    rule getTag(U32(_))        => 4 
+    rule getTag(U32(_))        => 4
     rule getTag(I32(_))        => 5
     rule getTag(U64(I))        => 6     requires          I <=Int #maxU64small
     rule getTag(U64(I))        => 64    requires notBool( I <=Int #maxU64small )
@@ -145,7 +172,7 @@ module HOST-OBJECT
     rule HostValOrDefault(X:HostVal, _:HostVal) => X
     rule HostValOrDefault(_,         D:HostVal) => D    [owise]
 
-    syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal     
+    syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal
         [function, total, symbol(List:getOrDefault)]
  // ---------------------------------------------------------
     rule OBJS {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ], D)
@@ -154,7 +181,7 @@ module HOST-OBJECT
     rule _OBJS {{ _I }} orDefault (D:ScVal) => D
       [owise]
 
-    syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal     
+    syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal
         [function, total, symbol(HostVal:getOrDefault)]
  // ---------------------------------------------------------
     rule OBJS {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D)
@@ -222,7 +249,7 @@ module HOST-OBJECT
     syntax String ::= decode6bit(Int)       [function, total, symbol(decode6bit)]
  // --------------------------------------------------------------------------------
     rule decode6bit(I) => decode6bit(I >>Int 6) +String decode6bitChar(I &Int 63)   requires 0 <Int I
-    rule decode6bit(_) => ""                                                        [owise] 
+    rule decode6bit(_) => ""                                                        [owise]
 
     syntax String ::= "sixBitStringTable" [macro]
  // -------------------------------------------------------------------------------------------
@@ -241,7 +268,7 @@ module HOST-OBJECT
       => encode6bitAux((A <<Int 6) |Int encode6bitChar(head(S)), tail(S))
       requires 0 <Int lengthString(S)
     rule encode6bitAux(A, _) => A
-      [owise] 
+      [owise]
 
     syntax Int ::= encode6bitChar(String)   [function, total, symbol(encode6bitChar)]
  // ---------------------------------------------------------------------------------
@@ -253,9 +280,9 @@ module HOST-OBJECT
     rule validSymbol(S) => true
       requires lengthString(S) ==Int 0
     rule validSymbol(S) => validSymbolChar(head(S)) andBool validSymbol(tail(S))
-      requires 0 <Int lengthString(S) andBool lengthString(S) <=Int 32 
+      requires 0 <Int lengthString(S) andBool lengthString(S) <=Int 32
     rule validSymbol(S) => false
-      requires 32 <Int lengthString(S) 
+      requires 32 <Int lengthString(S)
 
     rule validSymbolChar(I) => findChar(sixBitStringTable, I, 0) =/=Int -1
 
@@ -266,6 +293,6 @@ module HOST-OBJECT
     rule head(S) => substrString(S, 0, 1)                      requires lengthString(S) >Int 0
     rule tail(S) => ""                                         requires lengthString(S) <=Int 0
     rule tail(S) => substrString(S, 1, lengthString(S))        requires lengthString(S) >Int 0
-    
+
 endmodule
 ```
diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md
@@ -1,11 +1,13 @@
 
 ```k
 requires "integer.md"
+requires "map.md"
 requires "symbol.md"
 requires "vector.md"
 
 module HOSTFUNS
     imports HOST-INTEGER
+    imports HOST-MAP
     imports HOST-SYMBOL
     imports HOST-VECTOR
 endmodule