diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md
index acb4500..1179183 100644
--- 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]:
+ hostCallAux("m", "5")
+ => allocObject(sortedKeys(M) {{ I }} orDefault Void)
+ ~> returnHostVal
+ ...
+
+ ScMap(M) : U32(I) : S => S
+ requires 0 <=Int I
+ andBool I hostCallAux("m", "5")
+ => #throw(ErrObject, IndexBounds)
+ ...
+
+ ScMap(M) : U32(I) : S => S
+ requires I hostCallAux("m", "6")
+ => #let KEY = sortedKeys(M) {{ I }} orDefault Void
+ #in M {{ KEY }} orDefault HostVal(-1)
+ ...
+
+ ScMap(M) : U32(I) : S => S
+ requires 0 <=Int I
+ andBool I hostCallAux("m", "6")
+ => #throw(ErrObject, IndexBounds)
+ ...
+
+ ScMap(M) : U32(I) : S => S
+ requires I 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)
\ No newline at end of file
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
index 4d1e6ab..ae5338d 100644
--- 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 = 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
+ }
}