implement map_key_by_pos, map_val_by_pos

runtimeverification · Dec 19, 2024 · ca5465a · ca5465a
1 parent c292d14
commit ca5465a
Show file tree

Hide file tree

Showing 3 changed files with 182 additions and 1 deletion.
diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md
@@ -147,6 +147,58 @@ 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_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,17 @@ 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)))
 
   (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))
 )
 )
 
@@ -188,4 +192,106 @@ 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
+)
+
 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,27 @@ impl ContainersContract {
         true
     }
 
+    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);
+
+        // Iterate through the key-value pairs in the map, ensuring:
+        let mut cur = 0;
+        for (i, x) in map {
+            // Keys are strictly increasing
+            assert_eq!(cur, i);
+            assert_eq!(x, -(i as i32));
+
+            cur += 1;
+        }
+
+        true
+    }
 }