From e33a81453e69671ea9f094d6798f9d208f23e0cc Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 6 Dec 2024 15:37:58 +0300 Subject: [PATCH 1/8] implement ScVal comparison --- src/komet/kdist/soroban-semantics/data.md | 226 +++++++++++++++++- .../kdist/soroban-semantics/host/context.md | 23 +- 2 files changed, 225 insertions(+), 24 deletions(-) diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index 036651b..a4b43c6 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -47,7 +47,7 @@ various contexts: would be required if `HostVal` were used. * Outside the Host: * `ScVec`: Represented as a `List` of `ScVal`. - * `ScVec`: Represented as a `Map` from `ScVal` to `ScVal`. + * `ScMap`: Represented as a `Map` from `ScVal` to `ScVal`. ```k syntax ScVal @@ -60,8 +60,8 @@ various contexts: | I64(Int) [symbol(SCVal:I64)] | U128(Int) [symbol(SCVal:U128)] | I128(Int) [symbol(SCVal:I128)] - | ScVec(List) [symbol(SCVal:Vec)] // List - | ScMap(Map) [symbol(SCVal:Map)] // Map + | ScVec(List) [symbol(SCVal:Vec)] // List or List + | ScMap(Map) [symbol(SCVal:Map)] // Map or Map | ScAddress(Address) [symbol(SCVal:Address)] | Symbol(String) [symbol(SCVal:Symbol)] | ScBytes(Bytes) [symbol(SCVal:Bytes)] @@ -187,10 +187,10 @@ module HOST-OBJECT syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal [function, total, symbol(List:getOrDefault)] // --------------------------------------------------------- - rule OBJS {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ], D) + rule OBJS:List {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ], D) requires 0 <=Int I andBool I D + rule _OBJS:List {{ _I }} orDefault (D:ScVal) => D [owise] syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal @@ -208,6 +208,11 @@ module HOST-OBJECT // --------------------------------------------------------- rule OBJS:Map {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ] orDefault D, D) + // typed version of builtin MAP [ K ] orDefault V + syntax ScVal ::= Map "{{" KItem "}}" "orDefault" ScVal + [function, total, symbol(ScVal:lookupOrDefault)] + // --------------------------------------------------------- + rule OBJS:Map {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ] orDefault D, D) ``` ## Conversion between `HostVal` and `ScVal` @@ -344,5 +349,216 @@ module HOST-OBJECT rule #pow(i128) => 340282366920938463463374607431768211456 rule #pow1(i128) => 170141183460469231731687303715884105728 +``` + +## Value Comparison + +[CAP 46-1: Comparison](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#comparison) + +```k + syntax Ordering ::= "Less" [symbol(Ordering:Less)] + | "Equal" [symbol(Ordering:Equal)] + | "Greater" [symbol(Ordering:Greater)] + + syntax Int ::= Ordering2Int(Ordering) [function, total] + // ----------------------------------------------------------- + rule Ordering2Int(Less) => -1 + rule Ordering2Int(Equal) => 0 + rule Ordering2Int(Greater) => 1 +``` + +- `compare(A, B)`: Defines a total order between `ScVal`s. + + +```k + syntax Ordering ::= compare(ScVal, ScVal) [function, total, symbol(compare)] +``` + +If `A` and `B` belong to different variants, their order is determined by the function `ScValTypeOrd(_:ScVal)`. +`ScValTypeOrd` assigns a unique precedence to each variant type. + +```k + rule compare(A, B) => compareInt(ScValTypeOrd(A), ScValTypeOrd(B)) + requires ScValTypeOrd(A) =/=Int ScValTypeOrd(B) +``` + +If `A` and `B` are of the same variant, they are compared by their underlying values. +For scalar types the comparison is straightforward. + +```k + rule compare(SCBool(A), SCBool(B)) => compareBool(A, B) + rule compare(Void, Void) => Equal + rule compare(Error(ATYP, ACODE), Error(BTYP, BCODE)) + => #if ATYP ==K BTYP + #then compareInt(ACODE, BCODE) + #else compareInt(ErrorType2Int(ATYP), ErrorType2Int(BTYP)) + #fi + rule compare(U32(A), U32(B)) => compareInt(A, B) + rule compare(I32(A), I32(B)) => compareInt(A, B) + rule compare(U64(A), U64(B)) => compareInt(A, B) + rule compare(I64(A), I64(B)) => compareInt(A, B) + rule compare(U128(A), U128(B)) => compareInt(A, B) + rule compare(I128(A), I128(B)) => compareInt(A, B) + rule compare(ScAddress(A), ScAddress(B)) => compareAddress(A, B) + rule compare(Symbol(A), Symbol(B)) => compareString(A, B) + rule compare(ScBytes(A), ScBytes(B)) => compareBytes(A, B) +``` + +For container types, the comparison is recursive as defined in `compareVec` and `compareMap`. + +- Maps are compared key-by-key in sorted or der of keys +- Vectors are compared element-by-element in order + +```k + rule compare(ScVec(A), ScVec(B)) => compareVec(A, B) + rule compare(ScMap(A), ScMap(B)) => compareMap(A, sortedKeys(A), B, sortedKeys(B)) +``` + +### Comparison of scalars + +```k + syntax Ordering ::= compareBool(Bool, Bool) [function, total, symbol(compareBool)] + // ---------------------------------------------------------------------------------------------- + rule compareBool(true, true) => Equal + rule compareBool(true, false) => Greater + rule compareBool(false,true) => Less + rule compareBool(false,false) => Equal + + syntax Ordering ::= compareAddress(Address, Address) [function, total, symbol(compareAddress)] + // ------------------------------------------------------------------------------------- + rule compareAddress(Account(_), Contract(_)) => Less + rule compareAddress(Contract(_), Account(_)) => Greater + rule compareAddress(Contract(A), Contract(B)) => compareBytes(A, B) + rule compareAddress(Account(A), Account(B)) => compareBytes(A, B) + + syntax Ordering ::= compareBytes(Bytes, Bytes) [function, total, symbol(compareBytes)] + | compareString(String, String) [function, total, symbol(compareString)] + // --------------------------------------------------------------------------------------------- + rule compareBytes(A, B) => compareString(Bytes2String(A), Bytes2String(B)) + rule compareString(A, B) => Less requires A Equal requires A ==String B + rule compareString(A, B) => Greater requires A >String B + + syntax Ordering ::= compareInt(Int, Int) [function, total] + // ------------------------------------------------------------ + rule compareInt(A, B) => Less requires A Equal requires A ==Int B + rule compareInt(A, B) => Greater requires A >Int B + +``` + +### Comparison of vectors (`compareVec`) + +The `compareVec` function compares two lists of `ScVal` values element by element, determining their order based on the +first differing element. If one list is shorter, it is considered smaller; if all elements are equal, the lists are equal. +If a list contains an element that is not an `ScVal`, which should not occur, the function returns a default value of +`Equal` to remain total. + +```k + syntax Ordering ::= compareVec(List, List) [function, total, symbol(compareVec)] + // ----------------------------------------------------------------------------- + rule compareVec(.List, .List ) => Equal + rule compareVec(.List, ListItem(_:ScVal) _) => Less + rule compareVec(ListItem(_:ScVal) _, .List ) => Greater + rule compareVec(ListItem(A) AS, ListItem(B) BS) + => #let C = compare(A, B) #in + #if C =/=K Equal + #then C + #else compareVec(AS, BS) + #fi + // invalid type + rule compareVec(_, _) => Equal [owise] +``` + +### Comparison of maps (`compareMap`) + +The `compareMap` function compares two maps by iterating through their sorted keys and comparing the keys and +corresponding values. + +`compareMap(Map1, Keys1, Map2, Keys2)`: +- `Map1` and `Map2`: Two maps being compared +- `Keys1` and `Keys2`: Sorted lists of keys for the respective maps, the order in which entries are compared. + +```k + syntax Ordering ::= compareMap(map1: Map, keys1: List, map2: Map, keys2: List) + [function, total, symbol(compareMap)] + // ----------------------------------------------------------------------------------- + rule compareMap(_M1, .List, _M2, .List) => Equal + rule compareMap(_M1, .List, _M2, ListItem(_:ScVal) _) => Less + rule compareMap(_M1, ListItem(_:ScVal) _, _M2, .List) => Greater + rule compareMap(M1, ListItem(A) AS, M2, ListItem(B) BS) + => #let C = compareMapItem( A, M1 {{ A }} orDefault Void, B, M2 {{ B }} orDefault Void ) #in + #if C =/=K Equal + #then C + #else compareMap(M1, AS, M2, BS) + #fi + // invalid type + rule compareMap(_, _, _, _) => Equal [owise] + + + syntax Ordering ::= compareMapItem(key1: ScVal, val1: ScVal, key2: ScVal, val2: ScVal) [function, total] + // ----------------------------------------------------------------------------------------------------------- + rule compareMapItem(AK, AV, BK, BV) + => #let C = compare(AK, BK) #in + #if C =/=K Equal + #then C + #else compare(AV, BV) + #fi + + syntax Int ::= ScValTypeOrd(ScVal) [function, total, symbol(ScValTypeOrd)] + // ------------------------------------------------------------------------------------------------- + rule ScValTypeOrd(SCBool(_)) => 0 + rule ScValTypeOrd(Void) => 1 + rule ScValTypeOrd(Error(_,_)) => 2 + rule ScValTypeOrd(U32(_)) => 3 + rule ScValTypeOrd(I32(_)) => 4 + rule ScValTypeOrd(U64(_)) => 5 + rule ScValTypeOrd(I64(_)) => 6 + // Timepoint => 7 + // Duration => 8 + rule ScValTypeOrd(U128(_)) => 9 + rule ScValTypeOrd(I128(_)) => 10 + // U256 => 11 + // I256 => 12 + rule ScValTypeOrd(ScBytes(_)) => 13 + // String => 14 + rule ScValTypeOrd(Symbol(_)) => 15 + rule ScValTypeOrd(ScVec(_)) => 16 + rule ScValTypeOrd(ScMap(_)) => 17 + rule ScValTypeOrd(ScAddress(_)) => 18 + // ContractInstance => 19 + // LedgerKeyContractInstance => 20 + // LedgerKeyNonce => 21 +``` + +## Sorted key lists for ScMap + +### Insertion + +```k + syntax List ::= insertKey(ScVal, List) [function, total, symbol(insertKey)] + // ---------------------------------------------------------------------------------------------- + rule insertKey(KEY, ListItem(X) XS) => ListItem(X) insertKey(KEY, XS) + requires Less ==K compare(X, KEY) + rule insertKey(KEY, ListItem(X) XS) => ListItem(X) XS + requires Equal ==K compare(X, KEY) + rule insertKey(KEY, XS) => ListItem(KEY) XS + [owise] +``` + +### Creation + +```k + syntax List ::= sortedKeys(Map) [function, total] + // --------------------------------------------------- + rule sortedKeys(M) => sortKeys(keys_list(M)) + + syntax List ::= sortKeys(List) [function, total, symbol(sortKeys)] + // ------------------------------------------------------------------------- + rule sortKeys(ListItem(KEY:ScVal) REST) => insertKey(KEY, sortKeys(REST)) + rule sortKeys(.List) => .List + // sort mismatch + rule sortKeys(ListItem(_) _REST) => .List [owise] + endmodule ``` diff --git a/src/komet/kdist/soroban-semantics/host/context.md b/src/komet/kdist/soroban-semantics/host/context.md index 2e1a3cd..c57066a 100644 --- a/src/komet/kdist/soroban-semantics/host/context.md +++ b/src/komet/kdist/soroban-semantics/host/context.md @@ -21,29 +21,14 @@ module HOST-CONTEXT 0 |-> OBJ_A 1 |-> OBJ_B + requires isObject(HostVal(OBJ_A)) + orBool isObject(HostVal(OBJ_B)) - // TODO This only works for addresses. Implement it properly for other cases. - // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#comparison syntax InternalInstr ::= "objCmp" [symbol(objCmp)] // ---------------------------------------------------- rule [objCmp-equal]: - objCmp => i64.const compareAddress(A, B) ... - ScAddress(A) : ScAddress(B) : S => S - - syntax Int ::= compareAddress(Address, Address) [function, total, symbol(compareAddress)] - // ------------------------------------------------------------------------------------- - rule compareAddress(Account(_), Contract(_)) => -1 - rule compareAddress(Contract(_), Account(_)) => 1 - rule compareAddress(Contract(A), Contract(B)) => compareBytes(A, B) - rule compareAddress(Account(A), Account(B)) => compareBytes(A, B) - - syntax Int ::= compareBytes(Bytes, Bytes) [function, total, symbol(compareBytes)] - | compareString(String, String) [function, total, symbol(compareString)] - // ------------------------------------------------------------------------------------- - rule compareBytes(A, B) => compareString(Bytes2String(A), Bytes2String(B)) - rule compareString(A, B) => -1 requires A 0 requires A ==String B - rule compareString(A, B) => 1 requires A >String B + objCmp => i64.const Ordering2Int(compare(A, B)) ... + A : B : S => S ``` From c23b9e470f5bce105d00fa3b7c6bbfe0c42c72cc Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 6 Dec 2024 15:38:17 +0300 Subject: [PATCH 2/8] add test: compare.wast --- src/tests/integration/data/compare.wast | 119 ++++++++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 src/tests/integration/data/compare.wast diff --git a/src/tests/integration/data/compare.wast b/src/tests/integration/data/compare.wast new file mode 100644 index 0000000..fbbb790 --- /dev/null +++ b/src/tests/integration/data/compare.wast @@ -0,0 +1,119 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module + (import "x" "0" (func $obj_cmp (param i64 i64) (result i64))) + (func $small_i64_to_i64_val (param i64) (result i64) + local.get 0 + i64.const 8 + i64.shl + i64.const 7 + i64.or + ) + (func $is_object (param i64) (result i32) + local.get 0 + i32.wrap_i64 + i32.const -64 + i32.add + i32.const 255 + i32.and + i32.const 14 + i32.lt_u + ) + (func $compare (param i64 i64) (result i64) + block + local.get 0 + call $is_object + br_if 0 + local.get 1 + call $is_object + br_if 0 + i64.const 0 + call $small_i64_to_i64_val + return + end + (call $obj_cmp (local.get 0) (local.get 1)) + call $small_i64_to_i64_val + ) + (export "compare" (func $compare)) +) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(U64(1)) ListItem(U64(2)), + I64(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(U64(1)) ListItem(U64(1000000000000000000000000000000000)), + I64(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(U64(1000000000000000000000000000000000)) ListItem(U64(1000000000000000000000000000000000)), + I64(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(U64(1000000000000000000000000000000000)) ListItem(U64(1)), + I64(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(U64(1000000000000000000000000000000000)) ListItem(U64(2000000000000000000000000000000000)), + I64(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(U64(2000000000000000000000000000000000)) ListItem(U64(1000000000000000000000000000000000)), + I64(1) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(ScVec( ListItem(U32(1)) ListItem(U32(2)) ListItem(U32(3)) )) + ListItem(ScVec( ListItem(U32(1)) ListItem(U32(2)) )), + I64(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "compare", + ListItem(ScVec( ListItem(U32(1)) ListItem(U32(2)) ListItem(U32(3)) )) + ListItem(ScVec( ListItem(U32(2)) ListItem(U32(2)) )), + I64(-1) +) + +setExitCode(0) \ No newline at end of file From 863eabc9869c9998f1d1487144b02ec05a59b549 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 6 Dec 2024 15:38:36 +0300 Subject: [PATCH 3/8] add komet test for object comparison --- .../soroban/contracts/test_compare/Cargo.toml | 15 ++++ .../soroban/contracts/test_compare/src/lib.rs | 69 +++++++++++++++++++ 2 files changed, 84 insertions(+) create mode 100644 src/tests/integration/data/soroban/contracts/test_compare/Cargo.toml create mode 100644 src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs diff --git a/src/tests/integration/data/soroban/contracts/test_compare/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_compare/Cargo.toml new file mode 100644 index 0000000..ebf42dd --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_compare/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_compare" +version = "0.0.0" +edition = "2021" +publish = false + +[lib] +crate-type = ["cdylib"] +doctest = false + +[dependencies] +soroban-sdk = { workspace = true } + +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } diff --git a/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs new file mode 100644 index 0000000..bbcc351 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs @@ -0,0 +1,69 @@ +#![no_std] +use core::cmp::Ordering; + +use soroban_sdk::{contract, contractimpl, Address, Env, IntoVal, TryFromVal, Val, Vec}; + +#[contract] +pub struct CompareContract; + +// Compares two values of type `T` using host-side comparison semantics. +// The values are placed into vectors to ensure comparison is performed +// via `obj_cmp`, regardless of the type-specific behavior. +fn compare(e: &Env, a: T, b: T) -> Ordering + where T: TryFromVal + IntoVal +{ + let va = Vec::from_array(&e, [a]); + let vb = Vec::from_array(&e, [b]); + + va.cmp(&vb) +} + +#[contractimpl] +impl CompareContract { + pub fn test_address(_env: Env, a: Address, b: Address) -> bool { + let _ = a.cmp(&b); + true + } + + pub fn test_address_vec(env: Env, a: Address, b: Address) -> bool { + compare(&env, a.clone(), b.clone()) == a.cmp(&b) + } + + /// The `soroban_sdk` implements integer comparison on the Wasm side. This test + /// uses the `compare` function to ensure the integers are compared using the + /// `obj_cmp` host function. It then verifies that the result matches the + /// comparison performed by the SDK's guest-side implementation. + pub fn test_cmp_i128(env: Env, a: i128, b: i128) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_i64(env: Env, a: i64, b: i64) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_i32(env: Env, a: i32, b: i32) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_u128(env: Env, a: i128, b: i128) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_u64(env: Env, a: i64, b: i64) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_u32(env: Env, a: i32, b: i32) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_bool(env: Env, a: bool, b: bool) -> bool { + compare(&env, a, b) == a.cmp(&b) + } + + pub fn test_cmp_void(env: Env) -> bool { + let a = (); + let b = (); + compare(&env, a, b) == a.cmp(&b) + } +} From d4b522a0bc8e60a72dab9c15b997553632aae2dd Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 9 Dec 2024 10:18:16 +0000 Subject: [PATCH 4/8] Set Version: 0.1.46 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 6ee33ba..79e0dd8 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.45 +0.1.46 diff --git a/pyproject.toml b/pyproject.toml index e82e651..69d07f7 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.45" +version = "0.1.46" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From da803cd2408ddd7f1fd609168dec596ca34f7fa5 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 18 Dec 2024 14:10:48 +0300 Subject: [PATCH 5/8] add `Bytes` comparison property test --- .../soroban/contracts/test_compare/src/lib.rs | 30 ++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs index bbcc351..df33a76 100644 --- a/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs @@ -1,7 +1,7 @@ #![no_std] use core::cmp::Ordering; -use soroban_sdk::{contract, contractimpl, Address, Env, IntoVal, TryFromVal, Val, Vec}; +use soroban_sdk::{contract, contractimpl, Address, Bytes, Env, IntoVal, String, TryFromVal, Val, Vec}; #[contract] pub struct CompareContract; @@ -18,6 +18,10 @@ fn compare(e: &Env, a: T, b: T) -> Ordering va.cmp(&vb) } + +const ARR_LENGTH: usize = 512; + + #[contractimpl] impl CompareContract { pub fn test_address(_env: Env, a: Address, b: Address) -> bool { @@ -66,4 +70,28 @@ impl CompareContract { let b = (); compare(&env, a, b) == a.cmp(&b) } + + /// Checks whether the comparison of two `Bytes` values produces the + /// same result as comparing their corresponding slices after copying + pub fn test_cmp_bytes(_env: Env, a: Bytes, b: Bytes) -> bool { + // Initialize fixed-length arrays for storing byte data of `a` and `b`. + let mut arr_a = [0 as u8; ARR_LENGTH]; + let mut arr_b = [0 as u8; ARR_LENGTH]; + + // Assume the lengths of `a` and `b` don't exceed the limit + if a.len() as usize > ARR_LENGTH || b.len() as usize > ARR_LENGTH { + return true; + } + + // Copy the contents of `a` and `b` into their respective slices. + let slc_a = &mut arr_a[0..a.len() as usize]; + let slc_b = &mut arr_b[0..b.len() as usize]; + a.copy_into_slice(slc_a); + b.copy_into_slice(slc_b); + + // Compare `a` and `b` directly and check if the result matches the comparison + // of their corresponding slices + a.cmp(&b) == slc_a.cmp(&slc_b) + } + } From 109e4224e69ef3b1f39274a5b6c3a965546b6474 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 18 Dec 2024 14:11:13 +0300 Subject: [PATCH 6/8] implement `bytes_copy_to_linear_memory` --- src/komet/kdist/soroban-semantics/host/buffer.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/komet/kdist/soroban-semantics/host/buffer.md b/src/komet/kdist/soroban-semantics/host/buffer.md index f797750..a8e1323 100644 --- a/src/komet/kdist/soroban-semantics/host/buffer.md +++ b/src/komet/kdist/soroban-semantics/host/buffer.md @@ -14,6 +14,22 @@ module HOST-BUFFER ``` +## bytes_copy_to_linear_memory + +```k + rule [hostCallAux-bytes-copy-to-linear-memory]: + hostCallAux ( "b" , "1" ) + => #memStore(LM_POS, substrBytes(BYTES, B_POS, B_POS +Int LEN)) + ~> toSmall(Void) + ... + + ScBytes(BYTES) : U32(B_POS) : U32(LM_POS) : U32(LEN) : S => S + requires 0 <=Int B_POS + andBool B_POS <=Int lengthBytes(BYTES) + andBool 0 <=Int LEN + andBool B_POS +Int LEN <=Int lengthBytes(BYTES) +``` + ## bytes_new_from_linear_memory ```k From f56afaed8d8c2b4f78cd4d3bd604ccd0584c8920 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 18 Dec 2024 14:11:52 +0300 Subject: [PATCH 7/8] add komet test for `bytes_copy_to_linear_memory` --- .../contracts/test_hostfuns/Cargo.toml | 15 +++++++++ .../contracts/test_hostfuns/src/lib.rs | 31 +++++++++++++++++++ 2 files changed, 46 insertions(+) create mode 100644 src/tests/integration/data/soroban/contracts/test_hostfuns/Cargo.toml create mode 100644 src/tests/integration/data/soroban/contracts/test_hostfuns/src/lib.rs diff --git a/src/tests/integration/data/soroban/contracts/test_hostfuns/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_hostfuns/Cargo.toml new file mode 100644 index 0000000..2a9fdfa --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_hostfuns/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_hostfuns" +version = "0.0.0" +edition = "2021" +publish = false + +[lib] +crate-type = ["cdylib"] +doctest = false + +[dependencies] +soroban-sdk = { workspace = true } + +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } diff --git a/src/tests/integration/data/soroban/contracts/test_hostfuns/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_hostfuns/src/lib.rs new file mode 100644 index 0000000..c33bc73 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_hostfuns/src/lib.rs @@ -0,0 +1,31 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, Bytes, Env}; + +#[contract] +pub struct TestHostfunsContract; + +const ARR_LENGTH: usize = 512; + +#[contractimpl] +impl TestHostfunsContract { + + // Validate the roundtrip conversion of a `Bytes` value into a slice. + // Tests the 'bytes_copy_to_linear_memory' and + // 'bytes_new_from_linear_memory' host functions + pub fn test_bytes_slice_roundtrip(env: Env, a: Bytes) -> bool { + let mut arr_a = [0 as u8; ARR_LENGTH]; + + if a.len() as usize > ARR_LENGTH { + return true; + } + + let mut slc_a = &mut arr_a[0..a.len() as usize]; + // bytes_copy_to_linear_memory + a.copy_into_slice(&mut slc_a); + + // bytes_new_from_linear_memory + let a2 = Bytes::from_slice(&env, slc_a); + + a == a2 + } +} From d9e87dc647b557a2a938647c88b819fdba3f2644 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 18 Dec 2024 14:21:04 +0300 Subject: [PATCH 8/8] add more comments for `test_cmp_bytes` --- .../data/soroban/contracts/test_compare/src/lib.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs index df33a76..5f2dfba 100644 --- a/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_compare/src/lib.rs @@ -72,7 +72,16 @@ impl CompareContract { } /// Checks whether the comparison of two `Bytes` values produces the - /// same result as comparing their corresponding slices after copying + /// same result as comparing their corresponding slices after copying. + /// + /// In the Soroban host environment, `Bytes` host objects are compared + /// by their underlying slices. + /// + /// https://github.com/stellar/rs-soroban-env/blob/c1b238b65bfd13666be4ac14e0e390c31b549caf/soroban-env-host/src/host/comparison.rs#L63 + /// + /// This test verifies that the behavior of + /// `obj_cmp` for Bytes matches the behavior of comparing the byte slices + /// created from `Bytes` objects. pub fn test_cmp_bytes(_env: Env, a: Bytes, b: Bytes) -> bool { // Initialize fixed-length arrays for storing byte data of `a` and `b`. let mut arr_a = [0 as u8; ARR_LENGTH];