Merge branch 'master' into fxdao-ledger-hostfuns

deps/k_release

@@ -1 +1 @@
-7.1.165
+7.1.167

deps/kwasm_release

@@ -1 +1 @@
-0.1.112
+0.1.113

flake.nix

@@ -2,7 +2,7 @@
   description = "komet - K tooling for the Soroban platform";
 
   inputs = {
-    wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.112";
+    wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.113";
     k-framework.follows = "wasm-semantics/k-framework";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";

package/version

@@ -1 +1 @@
-0.1.39
+0.1.40

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.39"
+version = "0.1.40"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -18,7 +18,7 @@ soroban-semantics = "komet.kdist.plugin"
 
 [tool.poetry.dependencies]
 python = "^3.10"
-pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.112", subdirectory = "pykwasm" }
+pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.113", subdirectory = "pykwasm" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

src/komet/kdist/soroban-semantics/host/map.md

@@ -102,47 +102,5 @@ The function returns a `HostVal` pointing to the new map object.
         <relativeObjects> RELS </relativeObjects>
       requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8
 
-```
-
-## Helpers
-
-
-```k
-
-    syntax List ::= Bytes2U32List(Bytes)    [function, total, symbol(Bytes2U32List)]
- // --------------------------------------------------------------------------------
-    rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned))
-                              Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS)))
-      requires lengthBytes(BS) >=Int 4
-    rule Bytes2U32List(BS) => .List
-      requires lengthBytes(BS) <Int 4
-
-```
-
-- `loadSlices`: Load symbols stored as byte slices in Wasm memory.
-
-```k
-    syntax InternalInstr ::= "loadSlices"                     [symbol(loadSlices)]
-                           | loadSlicesAux(List)              [symbol(loadSlicesAux)]
- // ---------------------------------------------------------------------------------
-    rule [loadSlices]:
-        <instrs> loadSlices
-              => loadSlicesAux(Bytes2U32List(KEY_SLICES))
-              ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8)
-                 ...
-        </instrs>
-        <hostStack> KEY_SLICES : S => S </hostStack>
-
-    rule [loadSlicesAux-empty]:
-        <instrs> loadSlicesAux(.List) => .K ... </instrs>
-
-    rule [loadSlicesAux]:
-        <instrs> loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN))
-              => #memLoad(OFFSET, LEN)
-              ~> mkSymbolFromStack
-              ~> loadSlicesAux(REST)
-                 ...
-        </instrs>
-
 endmodule
 ```

src/komet/kdist/soroban-semantics/host/symbol.md

@@ -11,8 +11,11 @@ module HOST-SYMBOL
     imports WASM-OPERATIONS
     imports HOST-INTEGER
     imports SWITCH-SYNTAX
+```
 
-    // symbol_new_from_linear_memory
+## symbol_new_from_linear_memory
+
+```k
     rule [hostfun-symbol-new-from-linear-memory]:
         <instrs> hostCall ( "b" , "j" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
               => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN)))
@@ -38,11 +41,105 @@ module HOST-SYMBOL
         <hostStack> BS:Bytes : S => S </hostStack>
       requires validSymbol(Bytes2String(BS))
 
+  // TODO add validity check
     syntax InternalInstr ::= "mkSymbolFromStack"   [symbol(mkSymbolFromStack)]
  // ---------------------------------------------------------------------------------
     rule [mkSymbolFromStack]:
         <instrs> mkSymbolFromStack => .K ... </instrs>
         <hostStack> (BS => Symbol(Bytes2String(BS))) : _ </hostStack>
+```
+
+## symbol_index_in_linear_memory
+
+Linear search a `Symbol` in an array of byte slices. Return the index of the element or trap if not found.
+
+```k
+    rule [hostfun-symbol-index-in-linear-memory]:
+        <instrs> hostCall ( "b" , "m" , [ i64  i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(SYMBOL))
+              ~> #memLoad(getMajor(HostVal(POS)), 8 *Int getMajor(HostVal(LEN)))
+              ~> loadSlices
+              ~> symbolIndexInLinearMemory
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > SYMBOL    // Symbol
+          1 |-> < i64 > POS       // U32VAL
+          2 |-> < i64 > LEN       // U32VAL
+        </locals>
+      requires fromSmallValid(HostVal(POS))
+       andBool fromSmallValid(HostVal(LEN))
+
+    syntax InternalInstr ::= "symbolIndexInLinearMemory"            [symbol(symbolIndexInLinearMemory)]
+                           | symbolIndexInLinearMemoryAux(Int)      [symbol(symbolIndexInLinearMemoryAux)]
+ // ------------------------------------------------------------------------------------------------------
+    rule [symbolIndexInLinearMemory]:
+        <instrs> symbolIndexInLinearMemory
+              => symbolIndexInLinearMemoryAux(indexOf(HAYSTACK, NEEDLE))
+                 ...
+        </instrs>
+        <hostStack> NEEDLE:List : (Symbol(_) #as HAYSTACK) : S => S </hostStack>
+
+    rule [symbolIndexInLinearMemoryAux-trap]:
+        <instrs> symbolIndexInLinearMemoryAux(-1) => trap ... </instrs>
+
+    rule [symbolIndexInLinearMemoryAux]:
+        <instrs> symbolIndexInLinearMemoryAux(N) => toSmall(U32(N)) ... </instrs>
+      requires N =/=Int -1
+
+```
+
+## Helpers
+
+
+```k
+
+    syntax List ::= Bytes2U32List(Bytes)    [function, total, symbol(Bytes2U32List)]
+ // --------------------------------------------------------------------------------
+    rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned))
+                              Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS)))
+      requires lengthBytes(BS) >=Int 4
+    rule Bytes2U32List(BS) => .List
+      requires lengthBytes(BS) <Int 4
+
+```
+
+- `loadSlices`: Load symbols stored as byte slices in Wasm memory.
+
+```k
+    syntax InternalInstr ::= "loadSlices"                     [symbol(loadSlices)]
+                           | loadSlicesAux(List)              [symbol(loadSlicesAux)]
+ // ---------------------------------------------------------------------------------
+    rule [loadSlices]:
+        <instrs> loadSlices
+              => loadSlicesAux(Bytes2U32List(KEY_SLICES))
+              ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8)
+                 ...
+        </instrs>
+        <hostStack> KEY_SLICES : S => S </hostStack>
+
+    rule [loadSlicesAux-empty]:
+        <instrs> loadSlicesAux(.List) => .K ... </instrs>
+
+    rule [loadSlicesAux]:
+        <instrs> loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN))
+              => #memLoad(OFFSET, LEN)
+              ~> mkSymbolFromStack
+              ~> loadSlicesAux(REST)
+                 ...
+        </instrs>
+```
+
+- `indexOf(X, XS)`: returns the index of the first element in `XS` which is equal to `X`, or `-1` if there is no such element.
+
+```k
+    syntax Int ::= indexOf   (KItem, List)          [function, total, symbol(indexOf)]
+                 | indexOfAux(KItem, List, Int)     [function, total, symbol(indexOfAux)]
+ // --------------------------------------------------------------------------
+    rule indexOf(X, XS) => indexOfAux(X, XS, 0)
+    rule indexOfAux(_, .List,          _) => -1
+    rule indexOfAux(X, ListItem(Y) _,  N) => N                              requires X ==K  Y
+    rule indexOfAux(X, ListItem(Y) XS, N) => indexOfAux(X, XS, N +Int 1)    requires X =/=K Y
 
 endmodule
 ```

src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "test_custom_types"
+version = "0.0.0"
+edition = "2021"
+publish = false
+
+[lib]
+crate-type = ["cdylib"]
+doctest = false
+
+[dependencies]
+soroban-sdk = { workspace = true }
+
+[dev-dependencies]
+soroban-sdk = { workspace = true, features = ["testutils"] }

src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs

@@ -0,0 +1,50 @@
+#![no_std]
+use soroban_sdk::{contract, contractimpl, contracttype, symbol_short, Address, Bytes, Env, FromVal, Symbol, TryFromVal, TryIntoVal, Val, Vec, EnvBase};
+
+#[contract]
+pub struct TestCustomTypesContract;
+
+#[contracttype]
+#[derive(PartialEq)]
+pub enum MyBool {
+    True,
+    False
+}
+
+fn to_bool(p: &MyBool) -> bool {
+    match p {
+        MyBool::True => true,
+        MyBool::False => false
+    }
+}
+
+fn from_bool(p: bool) -> MyBool {
+    if p {
+        MyBool::True
+    } else {
+        MyBool::False
+    }
+}
+
+
+#[contractimpl]
+impl TestCustomTypesContract {
+
+    pub fn test_my_bool_roundtrip(env: Env, p: bool) -> bool {
+
+        // mp:MyBool lives in the Wasm memory
+        let mp = from_bool(p);
+
+        // convert MyBool to a host object
+        let v: Val = mp.try_into_val(&env).unwrap();
+
+        // convert v:Val to MyBool, load it to the Wasm memory
+        // (using the 'symbol_index_in_linear_memory' host function under the hood)
+        let mp2: MyBool = MyBool::try_from_val(&env, &v).unwrap();
+
+        let p2 = to_bool(&mp2);
+
+        mp == mp2 && p == p2
+    }
+
+}