Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Remaining Map Host Functions #54

Merged
merged 4 commits into from
Jan 10, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.47
0.1.48
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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]>",
Expand Down
82 changes: 82 additions & 0 deletions src/komet/kdist/soroban-semantics/host/map.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
163 changes: 163 additions & 0 deletions src/tests/integration/data/map.wast
Original file line number Diff line number Diff line change
Expand Up @@ -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))
)
)

Expand Down Expand Up @@ -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)
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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
}
}