From ca5465a1fa9a9714192528d4afd0dc9a29ef2ef3 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 19 Dec 2024 18:46:51 +0300 Subject: [PATCH 1/3] implement `map_key_by_pos`, `map_val_by_pos` --- src/komet/kdist/soroban-semantics/host/map.md | 52 +++++++++ src/tests/integration/data/map.wast | 106 ++++++++++++++++++ .../contracts/test_containers/src/lib.rs | 25 ++++- 3 files changed, 182 insertions(+), 1 deletion(-) 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 + } } From b393c0ba4e91780d20ecc127f616a8af857e95e5 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 19 Dec 2024 22:45:34 +0300 Subject: [PATCH 2/3] implement `map_keys` and `map_vals` --- src/komet/kdist/soroban-semantics/host/map.md | 30 ++++++++++ src/tests/integration/data/map.wast | 57 +++++++++++++++++++ .../contracts/test_containers/src/lib.rs | 15 ++++- 3 files changed, 100 insertions(+), 2 deletions(-) diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md index 1179183..c37af91 100644 --- a/src/komet/kdist/soroban-semantics/host/map.md +++ b/src/komet/kdist/soroban-semantics/host/map.md @@ -199,6 +199,36 @@ increasing order. Its primary use is alongside [`map_val_by_pos`](#map_val_by_po orBool size(M) <=Int I ``` +## map_keys + +```k + + rule [hostCallAux-map-keys]: + hostCallAux("m", "7") + => allocObject(ScVec(sortedKeys(M))) + ~> returnHostVal + ... + + ScMap(M) : S => S + +``` + +## map_vals + +```k + + rule [hostCallAux-map-vals]: + hostCallAux("m", "8") + => allocObject(ScVec( + lookupMany(M, sortedKeys(M), Void) + )) + ~> returnHostVal + ... + + ScMap(M) : S => S + +``` + ## 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 index 805e433..bbc395a 100644 --- a/src/tests/integration/data/map.wast +++ b/src/tests/integration/data/map.wast @@ -11,6 +11,8 @@ uploadWasm( b"test-wasm", (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)) @@ -20,6 +22,8 @@ uploadWasm( b"test-wasm", (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)) ) ) @@ -294,4 +298,57 @@ callTx( 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) \ 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 ae5338d..26eb2ad 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 @@ -26,6 +26,8 @@ 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; @@ -37,16 +39,25 @@ impl ContainersContract { } assert_eq!(map.len(), n); - // Iterate through the key-value pairs in the map, ensuring: + let vals = map.values(); + let keys = map.keys(); + 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; } + 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 } } From 069594e223b27396963e645600029d793ffe7a53 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 19 Dec 2024 19:57:01 +0000 Subject: [PATCH 3/3] Set Version: 0.1.48 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 9506d14..5946feb 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.47 +0.1.48 diff --git a/pyproject.toml b/pyproject.toml index c727f91..e6614b5 100644 --- 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. ",