Implement Remaining Map Host Functions (#54)

* implement `map_key_by_pos`, `map_val_by_pos` * implement `map_keys` and `map_vals` * Set Version: 0.1.48 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jan 10, 2025 · 19f8fcd · 19f8fcd
1 parent dcf6f8f
commit 19f8fcd
Show file tree

Hide file tree

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

diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md
@@ -147,6 +147,88 @@ module HOST-MAP
 
 ```
 
+## map_key_by_pos
+
+The `map_key_by_pos` function retrieves the **key** at a specified index from a sorted map, where keys are ordered in
+increasing order. Its primary use is alongside [`map_val_by_pos`](#map_val_by_pos) in map iterators within the Soroban SDK.
+
+```k
+
+    rule [hostCallAux-map-key-by-pos]:
+        <instrs> hostCallAux("m", "5")
+              => allocObject(sortedKeys(M) {{ I }} orDefault Void)
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : U32(I) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <Int size(M)
+
+
+    rule [hostCallAux-map-key-by-pos-err]:
+        <instrs> hostCallAux("m", "5")
+              => #throw(ErrObject, IndexBounds)
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : U32(I) : S => S </hostStack>
+      requires I <Int 0
+        orBool size(M) <=Int I
+```
+
+## map_val_by_pos
+
+```k
+
+    rule [hostCallAux-map-val-by-pos]:
+        <instrs> hostCallAux("m", "6")
+              => #let KEY = sortedKeys(M) {{ I }} orDefault Void
+                 #in M {{ KEY }} orDefault HostVal(-1)
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : U32(I) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <Int size(M)
+
+    rule [hostCallAux-map-val-by-pos-err]:
+        <instrs> hostCallAux("m", "6")
+              => #throw(ErrObject, IndexBounds)
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : U32(I) : S => S </hostStack>
+      requires I <Int 0
+        orBool size(M) <=Int I
+```
+
+## map_keys
+
+```k
+
+    rule [hostCallAux-map-keys]:
+        <instrs> hostCallAux("m", "7")
+              => allocObject(ScVec(sortedKeys(M)))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : S => S </hostStack>
+
+```
+
+## map_vals
+
+```k
+
+    rule [hostCallAux-map-vals]:
+        <instrs> hostCallAux("m", "8")
+              => allocObject(ScVec(
+                    lookupMany(M, sortedKeys(M), Void)
+                 ))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : S => S </hostStack>
+
+```
+
 ## map_unpack_to_linear_memory
 
 Writes values from a map (`ScMap`) to a specified memory address.

diff --git a/src/tests/integration/data/map.wast b/src/tests/integration/data/map.wast
@@ -9,13 +9,21 @@ uploadWasm( b"test-wasm",
   (import "m" "2" (func $del (param i64 i64)     (result i64)))
   (import "m" "3" (func $len (param i64)         (result i64)))
   (import "m" "4" (func $has (param i64 i64)     (result i64)))
+  (import "m" "5" (func $key_by_pos (param i64 i64) (result i64)))
+  (import "m" "6" (func $val_by_pos (param i64 i64) (result i64)))
+  (import "m" "7" (func $keys (param i64)        (result i64)))
+  (import "m" "8" (func $vals (param i64)        (result i64)))
 
   (export "new" (func $new))
   (export "put" (func $put))
   (export "get" (func $get))
   (export "del" (func $del))
   (export "len" (func $len))
   (export "has" (func $has))
+  (export "key_by_pos" (func $key_by_pos))
+  (export "val_by_pos" (func $val_by_pos))
+  (export "keys" (func $keys))
+  (export "vals" (func $vals))
 )
 )
 
@@ -188,4 +196,159 @@ callTx(
   )
 )
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; map_key_by_pos
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "key_by_pos",
+  ListItem(ScMap(
+    Symbol(str("foo")) |-> U32(1)
+  )) 
+  ListItem(U32(0)),
+  Symbol(str("foo"))
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "key_by_pos",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )) 
+  ListItem(U32(0)),
+  Symbol(str("a"))
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "key_by_pos",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )) 
+  ListItem(U32(1)),
+  Symbol(str("b"))
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "key_by_pos",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )) 
+  ListItem(U32(2)),
+  Error(ErrObject, 1) ;; IndexBounds
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; map_val_by_pos
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "val_by_pos",
+  ListItem(ScMap(
+    Symbol(str("foo")) |-> U32(1)
+  )) 
+  ListItem(U32(0)),
+  U32(1)
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "val_by_pos",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )) 
+  ListItem(U32(0)),
+  U32(2)
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "val_by_pos",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )) 
+  ListItem(U32(1)),
+  U32(1)
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "val_by_pos",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )) 
+  ListItem(U32(2)),
+  Error(ErrObject, 1) ;; IndexBounds
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; map_keys
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "keys",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )),
+  ScVec(
+    ListItem(Symbol(str("a")))
+    ListItem(Symbol(str("b")))
+  )
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "keys",
+  ListItem(ScMap(.Map)),
+  ScVec(.List)
+)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; map_vals
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "vals",
+  ListItem(ScMap(
+    Symbol(str("b")) |-> U32(1)
+    Symbol(str("a")) |-> U32(2)
+  )),
+  ScVec(
+    ListItem(U32(2))
+    ListItem(U32(1))
+  )
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "vals",
+  ListItem(ScMap(.Map)),
+  ScVec(.List)
+)
+
 setExitCode(0)
diff --git a/src/tests/integration/data/soroban/contracts/test_containers/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_containers/src/lib.rs
@@ -1,5 +1,5 @@
 #![no_std]
-use soroban_sdk::{contract, contractimpl, Env, Vec};
+use soroban_sdk::{contract, contractimpl, Env, Map, Vec};
 
 #[contract]
 pub struct ContainersContract;
@@ -26,4 +26,38 @@ impl ContainersContract {
         true
     }
 
+
+    // Iterate through the key-value pairs in the map ensuring keys are strictly increasing
+    pub fn test_map_iterate(env: Env, n: u32) -> bool {
+        let n = n % 100;
+
+        let mut map: Map<u32, i32> = Map::new(&env);
+        assert_eq!(map.len(), 0);
+
+        for i in (0..n).rev() {
+            map.set(i, -(i as i32));
+        }
+        assert_eq!(map.len(), n);
+
+        let vals = map.values();
+        let keys = map.keys();
+
+        let mut cur = 0;
+        for (i, x) in map {
+            assert_eq!(cur, i);
+            assert_eq!(x, -(i as i32));
+
+            cur += 1;
+        }
+
+        for (i, k) in keys.iter().enumerate() {
+            assert_eq!(k, i as u32);
+        }
+
+        for (i, x) in vals.iter().enumerate() {
+            assert_eq!(x, -(i as i32));
+        }
+
+        true
+    }
 }