Implement Vec and Symbol (#13)

* helpers for reading/writing wasm memory * implement `Vec` * Set Version: 0.1.7 * implement `Symbol` * fix validSymbol too long case * Set Version: 0.1.8 * Update src/ksoroban/kdist/soroban-semantics/wasm-ops.md Co-authored-by: gtrepta <[email protected]> * fix encode/decode small symbols and refactor Co-authored-by: gtrepta <[email protected]> --------- Co-authored-by: devops <[email protected]> Co-authored-by: gtrepta <[email protected]> Co-authored-by: gtrepta <[email protected]>
runtimeverification · Jul 23, 2024 · 9942796 · 9942796
1 parent f90cc8e
commit 9942796
Show file tree

Hide file tree

Showing 12 changed files with 824 additions and 35 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.7
+0.1.8
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.7"
+version = "0.1.8"
 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
@@ -46,7 +46,7 @@ module CONFIG
       </soroban>
 
     syntax HostStack ::= List{HostStackVal, ":"}  [symbol(hostStackList)]
-    syntax HostStackVal ::= ScVal | HostVal
+    syntax HostStackVal ::= ScVal | HostVal | Bytes
 
 
     syntax InternalCmd ::= #callResult(ValStack, List)   [symbol(#callResult)]
@@ -154,20 +154,54 @@ These internal commands manages the call stack when calling and returning from a
 
 ## `ScVal` Operations
 
-```k
+### 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 
+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 
     syntax InternalCmd ::= allocObject(ScVal)             [symbol(allocObject)]
  // ---------------------------------------------------------------------------
     rule [allocObject-small]:
         <k> allocObject(SCV) => .K ... </k>
         <hostStack> STACK => toSmall(SCV) : STACK </hostStack>
       requires toSmallValid(SCV)
 
+    // recursively allocate vector items
+    rule [allocObject-vec]:
+        <k> allocObject(ScVec(ITEMS))
+         => allocObjects(ITEMS)
+         ~> allocObjectVecAux
+            ...
+        </k>
+    
+    syntax InternalCmd ::= "allocObjectVecAux"
+ // ------------------------------------------
+    rule [allocObjectVecAux]:
+        <k> allocObjectVecAux => addObject(ScVec(V)) ... </k>
+        <hostStack> ScVec(V) : S => S </hostStack>
+
     rule [allocObject]:
-        <k> allocObject(SCV) => .K ... </k>
-        <hostObjects> OBJS => OBJS ListItem(SCV) </hostObjects>
-        <hostStack> STACK => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK </hostStack>
+        <k> allocObject(SCV) => addObject(SCV) ... </k>
       [owise]
 
+    // Allows using `allocObject` in the `<instrs>` cell
+    rule [allocObject-instr]:
+        <instrs> allocObject(SCV) => #waitCommands ... </instrs>
+        <k> (.K => allocObject(SCV)) ... </k>
+
+    syntax InternalCmd ::= addObject(ScVal)                                  [symbol(addObject)]
+ // --------------------------------------------------------------------------------------------
+    rule [addObject]:
+        <k> addObject(SCV) => .K ... </k>
+        <hostObjects> OBJS => OBJS ListItem(SCV) </hostObjects>
+        <hostStack> STACK
+                 => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK
+        </hostStack>
+
     syntax InternalCmd ::= allocObjects       (List)       [symbol(allocObjects)]
                          | allocObjectsAux    (List)       [symbol(allocObjectsAux)]
                          | allocObjectsCollect(Int)        [symbol(allocObjectsCollect)]
@@ -185,20 +219,23 @@ These internal commands manages the call stack when calling and returning from a
             ...
         </k>
 
+    rule [allocObjectsAux-HostVal]:
+        <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>
 
-    syntax HostStack ::= drop(Int, HostStack)   [function, total, symbol(HostStack:drop)]
- // -------------------------------------------------------------------------------------
-    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]
+```
+
+### Accessing host objects
+
 
+```k
     syntax InternalInstr ::= loadObject(HostVal)    [symbol(loadObject)]
  // --------------------------------------------------------------------
     rule [loadObject-abs]:
@@ -220,6 +257,28 @@ These internal commands manages the call stack when calling and returning from a
        andBool isRelativeObjectHandle(VAL)
        andBool 0 <=Int getIndex(VAL)
        andBool getIndex(VAL) <Int size(RELS)
+
+    rule [loadObject-small]:
+        <instrs> loadObject(VAL) => .K ... </instrs>
+        <hostStack> S => fromSmall(VAL) : S </hostStack>
+      requires notBool isObject(VAL)
+       andBool fromSmallValid(VAL)
+
+    
+```
+
+### Auxiliary functions
+
+```k
+    syntax HostStack ::= drop(Int, HostStack)   [function, total, symbol(HostStack:drop)]
+ // -------------------------------------------------------------------------------------
+    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]
 ```
 
 ## Call result handling
@@ -231,36 +290,47 @@ These internal commands manages the call stack when calling and returning from a
     rule [callResult]:
         <k> #callResult(<i64> I : SS, RELS)
          => #callResult(SS, RELS)
-         ~> HostVal2ScVal(HostVal(I), RELS)
+         ~> pushStack(HostVal2ScVal(HostVal(I), OBJS, RELS))
             ...
         </k>
-    
-    syntax InternalCmd ::= HostVal2ScVal(HostVal, List)      [symbol(HostVal2ScVal)]
- // --------------------------------------------------------------------------
-    rule [HostVal2ScVal-obj-abs]:
-        <k> HostVal2ScVal(VAL, _RELS) => .K ... </k>
         <hostObjects> OBJS </hostObjects>
-        <hostStack> S => OBJS {{ getIndex(VAL) }} orDefault Void : S </hostStack>
+    
+    // Convert HostVals to ScVal recursively
+    syntax ScVal ::= HostVal2ScVal(HostVal, objs: List, rels: List)      [function, total, symbol(HostVal2ScVal)]
+ // -------------------------------------------------------------------------------------------------------------------
+    rule HostVal2ScVal(VAL, OBJS, RELS) => HostVal2ScValRec(OBJS {{ getIndex(VAL) }} orDefault Void, OBJS, RELS)
       requires isObject(VAL)
        andBool notBool(isRelativeObjectHandle(VAL))
        andBool getIndex(VAL) <Int size(OBJS)
 
-    rule [HostVal2ScVal-obj-rel]:
-        <k> HostVal2ScVal(VAL, RELS)
-         => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), RELS)
-            ...
-        </k>
+    rule HostVal2ScVal(VAL, OBJS, RELS) => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), OBJS, RELS)
       requires isObject(VAL)
        andBool isRelativeObjectHandle(VAL)
        andBool getIndex(VAL) <Int size(RELS)
       [preserves-definedness]
 
-    rule [HostVal2ScVal-small]:
-        <k> HostVal2ScVal(VAL, _RELS) => .K ... </k>
-        <hostStack> S => fromSmall(VAL) : S </hostStack>
+    rule HostVal2ScVal(VAL, _OBJS, _RELS) => fromSmall(VAL)
       requires notBool isObject(VAL)
        andBool fromSmallValid(VAL)
 
+    rule HostVal2ScVal(_, _, _) => Void     [owise]
+
+    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(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
@@ -31,6 +31,7 @@ storing data on the host side.
         | ScVec(List)                              [symbol(SCVal:Vec)]
         | ScMap(Map)                               [symbol(SCVal:Map)]
         | ScAddress(Address)                       [symbol(SCVal:Address)]
+        | Symbol(String)                           [symbol(SCVal:Symbol)]
 
     syntax Address ::= AccountId | ContractId
     syntax AccountId  ::= Account(Bytes)          [symbol(AccountId)]
@@ -121,6 +122,9 @@ module HOST-OBJECT
     rule getTag(ScVec(_))      => 75
     rule getTag(ScMap(_))      => 76
     rule getTag(ScAddress(_))  => 77
+    rule getTag(Symbol(BS))    => 14    requires lengthString(BS) <=Int 9
+    rule getTag(Symbol(BS))    => 74    requires lengthString(BS) >Int  9
+
 
     // 64-bit integers that fit in 56 bits
     syntax Int ::= "#maxU64small"     [macro]
@@ -184,6 +188,9 @@ module HOST-OBJECT
 
     rule fromSmall(VAL) => U128(getBody(VAL))      requires getTag(VAL) ==Int 10
 
+    rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL)))
+                                                   requires getTag(VAL) ==Int 14
+
     // return `Void` for invalid values
     rule fromSmall(_) => Void    [owise]
 
@@ -201,15 +208,64 @@ module HOST-OBJECT
     rule toSmall(U32(I))        => fromMajorMinorAndTag(I, 0, 4)
     rule toSmall(I32(I))        => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5)
       requires definedUnsigned(i32, I)
-    rule toSmall(U64(I))        => fromBodyAndTag(I, 6)     requires I <=Int #maxU64small
-    rule toSmall(U128(I))       => fromBodyAndTag(I, 10)    requires I <=Int #maxU64small
-    rule toSmall(_)             => HostVal(-1)              [owise]      
+    rule toSmall(U64(I))        => fromBodyAndTag(I, 6)               requires I <=Int #maxU64small
+    rule toSmall(U128(I))       => fromBodyAndTag(I, 10)              requires I <=Int #maxU64small
+    rule toSmall(Symbol(S))     => fromBodyAndTag(encode6bit(S), 14)  requires lengthString(S) <=Int 9
+    rule toSmall(_)             => HostVal(-1)                        [owise]
 
     syntax Bool ::= toSmallValid(ScVal)
         [function, total, symbol(toSmallValid)]
  // ---------------------------------------------------------------------------------
     rule toSmallValid(VAL) => toSmall(VAL) =/=K HostVal(-1)
 
 
+    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] 
+
+    syntax String ::= "sixBitStringTable" [macro]
+ // -------------------------------------------------------------------------------------------
+    rule sixBitStringTable => "_0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefgyahijklmnopqrstuvwxyz"
+
+    syntax String ::= decode6bitChar(Int)   [function, total, symbol(decode6bitChar)]
+ // ---------------------------------------------------------------------------------
+    rule decode6bitChar(I) => substrString(sixBitStringTable, I -Int 1, I)
+
+    syntax Int ::= encode6bit   (     String)           [function, total, symbol(encode6bit)]
+                 | encode6bitAux(Int, String)           [function, total, symbol(encode6bitAux)]
+ // --------------------------------------------------------------------------------
+    rule encode6bit(S) => encode6bitAux(0, S)
+
+    rule encode6bitAux(A, S)
+      => encode6bitAux((A <<Int 6) |Int encode6bitChar(head(S)), tail(S))
+      requires 0 <Int lengthString(S)
+    rule encode6bitAux(A, _) => A
+      [owise] 
+
+    syntax Int ::= encode6bitChar(String)   [function, total, symbol(encode6bitChar)]
+ // ---------------------------------------------------------------------------------
+    rule encode6bitChar(I) => findChar(sixBitStringTable, I, 0) +Int 1
+
+    syntax Bool ::= validSymbol(String)          [function, total, symbol(validSymbol)]
+                  | validSymbolChar(String)      [function, total, symbol(validSymbolChar)]
+ // --------------------------------------------------------------------------------
+    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 
+    rule validSymbol(S) => false
+      requires 32 <Int lengthString(S) 
+
+    rule validSymbolChar(I) => findChar(sixBitStringTable, I, 0) =/=Int -1
+
+    syntax String ::= head(String)    [function, total, symbol(headString)]
+                    | tail(String)    [function, total, symbol(tailString)]
+ // -----------------------------------------------------------------------
+    rule head(S) => ""                                         requires lengthString(S) <=Int 0
+    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,8 +1,12 @@
 
 ```k
 requires "integer.md"
+requires "symbol.md"
+requires "vector.md"
 
 module HOSTFUNS
     imports HOST-INTEGER
+    imports HOST-SYMBOL
+    imports HOST-VECTOR
 endmodule
 ```
diff --git a/src/ksoroban/kdist/soroban-semantics/host/symbol.md b/src/ksoroban/kdist/soroban-semantics/host/symbol.md
@@ -0,0 +1,40 @@
+# Symbol
+
+```k
+requires "../configuration.md"
+requires "../switch.md"
+requires "../wasm-ops.md"
+requires "integer.md"
+
+module HOST-SYMBOL
+    imports CONFIG-OPERATIONS
+    imports WASM-OPERATIONS
+    imports HOST-INTEGER
+    imports SWITCH-SYNTAX
+
+    // symbol_new_from_linear_memory
+    rule [hostfun-symbol-new-from-linear-memory]:
+        <instrs> hostCall ( "b" , "j" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN)))
+              ~> symbolNewFromLinearMemory
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > LM_POS      // U32
+          1 |-> < i64 > LEN         // U32
+        </locals>
+      requires fromSmallValid(HostVal(LM_POS))
+       andBool fromSmallValid(HostVal(LEN))
+
+
+    syntax InternalInstr ::= "symbolNewFromLinearMemory"      [symbol(symbolNewFromLinearMemory)]
+    rule [symbolNewFromLinearMemory]:
+        <instrs> symbolNewFromLinearMemory
+              => allocObject(Symbol(Bytes2String(BS)))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> BS:Bytes : S => S </hostStack>
+      requires validSymbol(Bytes2String(BS))
+endmodule
+```