From d02f5f7505fa38411a6b4a86f4fee705cb3c76df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Sat, 27 Jul 2024 23:01:30 +0300 Subject: [PATCH] Implement `Map` (#15) * Implement `Map` * Set Version: 0.1.9 * add comments * map.md - reformat sections and comments * data.md - document ScVal * Set Version: 0.1.10 * ensure consistent order in `allocObject-map` --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- .../kdist/soroban-semantics/configuration.md | 104 +++-- src/ksoroban/kdist/soroban-semantics/data.md | 59 ++- .../kdist/soroban-semantics/host/hostfuns.md | 2 + .../kdist/soroban-semantics/host/map.md | 147 ++++++ .../kdist/soroban-semantics/host/symbol.md | 8 + .../kdist/soroban-semantics/kasmer.md | 6 +- src/tests/integration/data/structs.wast | 425 ++++++++++++++++++ 9 files changed, 706 insertions(+), 49 deletions(-) create mode 100644 src/ksoroban/kdist/soroban-semantics/host/map.md create mode 100644 src/tests/integration/data/structs.wast diff --git a/package/version b/package/version index 1a03094..9767cc9 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.9 +0.1.10 diff --git a/pyproject.toml b/pyproject.toml index aebcf3e..0ad22ff 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.9" +version = "0.1.10" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md index 449517a..aba1b07 100644 --- a/src/ksoroban/kdist/soroban-semantics/configuration.md +++ b/src/ksoroban/kdist/soroban-semantics/configuration.md @@ -26,7 +26,7 @@ module CONFIG .List // List of ScVals .List .List - + @@ -46,7 +46,7 @@ module CONFIG syntax HostStack ::= List{HostStackVal, ":"} [symbol(hostStackList)] - syntax HostStackVal ::= ScVal | HostVal | Bytes + syntax HostStackVal ::= ScVal | HostVal | Bytes | List syntax InternalCmd ::= #callResult(ValStack, List) [symbol(#callResult)] @@ -81,7 +81,7 @@ module CONFIG-OPERATIONS ## Call State -The `` cell stores a list of previous contract execution states. +The `` cell stores a list of previous contract execution states. These internal commands manages the call stack when calling and returning from a contract. ```k @@ -156,13 +156,13 @@ These internal commands manages the call stack when calling and returning from a ### Creating host objects -If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object -and pushes a `HostVal` onto the `` that points to the newly created object. -If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content +If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object +and pushes a `HostVal` onto the `` that points to the newly created object. +If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content but only pushes a single `HostVal` for the entire container onto the stack. If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly equivalent to `SCV`. - -```k + +```k syntax InternalCmd ::= allocObject(ScVal) [symbol(allocObject)] // --------------------------------------------------------------------------- rule [allocObject-small]: @@ -177,12 +177,40 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly ~> allocObjectVecAux ... - - syntax InternalCmd ::= "allocObjectVecAux" - // ------------------------------------------ + + // recursively allocate map values. + rule [allocObject-map]: + allocObject(ScMap(ITEMS)) + // Using `lookupMany` with `keys_list` instead of `values` + // to ensure the order of values matches the order of keys. + => allocObjects(lookupMany(ITEMS, keys_list(ITEMS), 0)) + ~> allocObjectMapAux(keys_list(ITEMS)) + ... + + + syntax Map ::= mapFromLists(List, List) [function, total, symbol(mapFromLists)] + // -------------------------------------------------------------------------------- + rule mapFromLists(ListItem(KEY) KEYS, ListItem(VAL) VALS) + => mapFromLists(KEYS, VALS) [ KEY <- VAL] + + rule mapFromLists(_, _) => .Map + [owise] + + syntax InternalCmd ::= "allocObjectVecAux" [symbol(allocObjectVecAux)] + // ------------------------------------------------------------------------- rule [allocObjectVecAux]: allocObjectVecAux => addObject(ScVec(V)) ... - ScVec(V) : S => S + V : S => S + + syntax InternalCmd ::= allocObjectMapAux(List) [symbol(allocObjectMapAux)] + // ------------------------------------------------------------------------- + rule [allocObjectMapAux]: + allocObjectMapAux(KEYS) + => addObject(ScMap(mapFromLists(KEYS, VALS))) + ... + + VALS : S => S + requires size(KEYS) ==Int size(VALS) rule [allocObject]: allocObject(SCV) => addObject(SCV) ... @@ -204,31 +232,37 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly syntax InternalCmd ::= allocObjects (List) [symbol(allocObjects)] | allocObjectsAux (List) [symbol(allocObjectsAux)] - | allocObjectsCollect(Int) [symbol(allocObjectsCollect)] // --------------------------------------------------------------------------- rule [allocObjects]: - allocObjects(L) => allocObjectsAux(L) ~> allocObjectsCollect(size(L)) ... + allocObjects(L) => allocObjectsAux(L) ~> collectStackObjects(size(L)) ... rule [allocObjectsAux-empty]: allocObjectsAux(.List) => .K ... rule [allocObjectsAux]: - allocObjectsAux(ListItem(SCV:ScVal) L) + allocObjectsAux(ListItem(SCV:ScVal) L) => allocObjectsAux(L) ~> allocObject(SCV) ... rule [allocObjectsAux-HostVal]: - allocObjectsAux(ListItem(HV:HostVal) L) + allocObjectsAux(ListItem(HV:HostVal) L) => allocObjectsAux(L) ~> pushStack(HV) ... - rule [allocObjectsCollect]: - allocObjectsCollect(LENGTH) => .K ... - STACK => ScVec(take(LENGTH, STACK)) : drop(LENGTH, STACK) + // Collect stack values into a List + syntax InternalCmd ::= collectStackObjects(Int) [symbol(collectStackObjects)] + // --------------------------------------------------------------------------------------- + rule [collectStackObjects]: + collectStackObjects(LENGTH) => .K ... + STACK => take(LENGTH, STACK) : drop(LENGTH, STACK) + + rule [collectStackObjects-instr]: + collectStackObjects(LENGTH) => .K ... + STACK => take(LENGTH, STACK) : drop(LENGTH, STACK) ``` @@ -248,7 +282,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly andBool getIndex(VAL) loadObject(VAL) + loadObject(VAL) => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0)) ... @@ -264,7 +298,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly requires notBool isObject(VAL) andBool fromSmallValid(VAL) - + ``` ### Auxiliary functions @@ -274,19 +308,29 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly // ------------------------------------------------------------------------------------- rule drop(N, _ : S) => drop(N -Int 1, S) requires N >Int 0 rule drop(_, S) => S [owise] - + syntax List ::= take(Int, HostStack) [function, total, symbol(HostStack:take)] // ------------------------------------------------------------------------------------- rule take(N, X : S) => ListItem(X) take(N -Int 1, S) requires N >Int 0 rule take(_, _) => .List [owise] ``` +- `lookupMany`: Retrieve values for multiple keys from a map. Return the specified default value for missing keys. + +```k + syntax List ::= lookupMany(Map, List, KItem) [function, total] + // ---------------------------------------------------------------- + rule lookupMany(M, ListItem(A) REST, D) => ListItem(M [ A ] orDefault D) lookupMany(M, REST, D) + rule lookupMany(_, _, _) => .List + [owise] +``` + ## Call result handling ```k rule [callResult-empty]: #callResult(.ValStack, _RELS) => .K ... - + rule [callResult]: #callResult( I : SS, RELS) => #callResult(SS, RELS) @@ -294,7 +338,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly ... OBJS - + // Convert HostVals to ScVal recursively syntax ScVal ::= HostVal2ScVal(HostVal, objs: List, rels: List) [function, total, symbol(HostVal2ScVal)] // ------------------------------------------------------------------------------------------------------------------- @@ -318,19 +362,23 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly syntax ScVal ::= HostVal2ScValRec(ScVal, objs: List, rels: List) [function, total, symbol(HostVal2ScValRec)] // ------------------------------------------------------------------------------------------------------------------- rule HostVal2ScValRec(ScVec(VEC), OBJS, RELS) => ScVec(HostVal2ScValMany(VEC, OBJS, RELS)) + + rule HostVal2ScValRec(ScMap(M), OBJS, RELS) + => ScMap(mapFromLists( keys_list(M), HostVal2ScValMany(values(M), OBJS, RELS)) ) + rule HostVal2ScValRec(SCV, _OBJS, _RELS) => SCV [owise] - + syntax List ::= HostVal2ScValMany(List, objs: List, rels: List) [function, total, symbol(HostVal2ScValMany)] // ------------------------------------------------------------------------------------------------------------------- rule HostVal2ScValMany(ListItem(V:HostVal) REST, OBJS, RELS) => ListItem(HostVal2ScVal(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS) - + rule HostVal2ScValMany(ListItem(V:ScVal) REST, OBJS, RELS) => ListItem(HostVal2ScValRec(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS) - + rule HostVal2ScValMany(_, _, _) => .List [owise] - + ``` ```k diff --git a/src/ksoroban/kdist/soroban-semantics/data.md b/src/ksoroban/kdist/soroban-semantics/data.md index 9b72912..27356cf 100644 --- a/src/ksoroban/kdist/soroban-semantics/data.md +++ b/src/ksoroban/kdist/soroban-semantics/data.md @@ -1,3 +1,4 @@ +# Host Data Types [Documentation - Host Value Type](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type) @@ -15,12 +16,38 @@ module HOST-OBJECT-SYNTAX [Documentation: ScVal](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#scval) -`ScVal` is a union of various datatypes used in the context of smart contracts for passing values to and from contracts and -storing data on the host side. +`ScVal` is a union of various datatypes used in the context of smart contracts for passing values to and from contracts +and storing data on the host side. +It combines elements from Stellar XDR’s `ScVal` and the Soroban Rust environment’s `HostObject` type (_Stellar XDR_ is +the data format storing and communicating blockchain data). +* [Stellar XDR - `ScVal`](https://github.com/stellar/stellar-xdr/blob/78ef9860777bd53e75a8ce8b978131cade26b321/Stellar-contract.x#L214) +* [Soroban Environment - `HostObject`](https://github.com/stellar/rs-soroban-env/blob/00ddd2714e757d0005bfc98798f05aa209f283bf/soroban-env-host/src/host_object.rs#L22) + +There are notable differences between XDR’s `ScVal` and Rust’s `HostObject`: + +* Data Representation: XDR `ScVal` and Rust `HostObject` differ in their data representation and storage. + XDR’s `ScVal` is recursive on container types such as map and vector, meaning it stores `ScVal`s as both keys and + values within vectors and maps, allowing for nested data structures. In contrast, `HostObject` uses `HostVal` in + container types, which requires resolving the corresponding host objects when accessing these values. +* Containers: XDR uses sorted vectors of key-value pairs for maps with binary search for lookups. The Rust environment + also uses a sorted vector but stores `HostVal` within these containers. Our semantics, however, use `Map` instead for + efficient lookup and simpler implementation. + +In our semantic implementation, `ScVal` is utilized to represent both XDR `ScVal` and Rust `HostObject`, adapting to +various contexts: + +* Inside the Host: + * `ScVec`: Represented as a `List` of `HostVal` + * `ScMap`: Represented as a `Map` from `ScVal` to `HostVal`. + Using `ScVal` as keys allows for more efficient lookups because it avoids the additional layer of indirection that + 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`. ```k - syntax ScVal + syntax ScVal ::= SCBool(Bool) [symbol(SCVal:Bool)] | "Void" [symbol(SCVal:Void)] | U32(Int) [symbol(SCVal:U32)] @@ -28,8 +55,8 @@ storing data on the host side. | U64(Int) [symbol(SCVal:U64)] | I64(Int) [symbol(SCVal:I64)] | U128(Int) [symbol(SCVal:U128)] - | ScVec(List) [symbol(SCVal:Vec)] - | ScMap(Map) [symbol(SCVal:Map)] + | ScVec(List) [symbol(SCVal:Vec)] // List + | ScMap(Map) [symbol(SCVal:Map)] // Map | ScAddress(Address) [symbol(SCVal:Address)] | Symbol(String) [symbol(SCVal:Symbol)] @@ -78,11 +105,11 @@ module HOST-OBJECT rule getBody(HostVal(I)) => I >>Int 8 syntax Bool ::= isObject(HostVal) [function, total, symbol(isObject)] - | isObjectTag(Int) [function, total, symbol(isObjectTag)] + | isObjectTag(Int) [function, total, symbol(isObjectTag)] | isRelativeObjectHandle(HostVal) [function, total, symbol(isRelativeObjectHandle)] // -------------------------------------------------------------------------------- rule isObject(V) => isObjectTag(getTag(V)) - rule isObjectTag(TAG) => 64 <=Int TAG andBool TAG <=Int 77 + rule isObjectTag(TAG) => 64 <=Int TAG andBool TAG <=Int 77 rule isRelativeObjectHandle(V) => getMajor(V) &Int 1 ==Int 0 syntax Int ::= indexToHandle(Int, Bool) [function, total, symbol(indexToHandle)] @@ -93,7 +120,7 @@ module HOST-OBJECT syntax Int ::= getIndex(HostVal) [function, total, symbol(getIndex)] // ---------------------------------------------------------------------------- rule getIndex(V) => getMajor(V) >>Int 1 - + syntax HostVal ::= fromHandleAndTag(Int, Int) [function, total, symbol(fromHandleAndTag)] | fromMajorMinorAndTag(Int, Int, Int) [function, total, symbol(fromMajorMinorAndTag)] | fromBodyAndTag(Int, Int) [function, total, symbol(fromBodyAndTag)] @@ -112,7 +139,7 @@ module HOST-OBJECT rule getTag(SCBool(true)) => 0 rule getTag(SCBool(false)) => 1 rule getTag(Void) => 2 - rule getTag(U32(_)) => 4 + rule getTag(U32(_)) => 4 rule getTag(I32(_)) => 5 rule getTag(U64(I)) => 6 requires I <=Int #maxU64small rule getTag(U64(I)) => 64 requires notBool( I <=Int #maxU64small ) @@ -145,7 +172,7 @@ module HOST-OBJECT rule HostValOrDefault(X:HostVal, _:HostVal) => X rule HostValOrDefault(_, D:HostVal) => D [owise] - syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal + syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal [function, total, symbol(List:getOrDefault)] // --------------------------------------------------------- rule OBJS {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ], D) @@ -154,7 +181,7 @@ module HOST-OBJECT rule _OBJS {{ _I }} orDefault (D:ScVal) => D [owise] - syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal + syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal [function, total, symbol(HostVal:getOrDefault)] // --------------------------------------------------------- rule OBJS {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D) @@ -222,7 +249,7 @@ module HOST-OBJECT syntax String ::= decode6bit(Int) [function, total, symbol(decode6bit)] // -------------------------------------------------------------------------------- rule decode6bit(I) => decode6bit(I >>Int 6) +String decode6bitChar(I &Int 63) requires 0 "" [owise] + rule decode6bit(_) => "" [owise] syntax String ::= "sixBitStringTable" [macro] // ------------------------------------------------------------------------------------------- @@ -241,7 +268,7 @@ module HOST-OBJECT => encode6bitAux((A < A - [owise] + [owise] syntax Int ::= encode6bitChar(String) [function, total, symbol(encode6bitChar)] // --------------------------------------------------------------------------------- @@ -253,9 +280,9 @@ module HOST-OBJECT rule validSymbol(S) => true requires lengthString(S) ==Int 0 rule validSymbol(S) => validSymbolChar(head(S)) andBool validSymbol(tail(S)) - requires 0 false - requires 32 findChar(sixBitStringTable, I, 0) =/=Int -1 @@ -266,6 +293,6 @@ module HOST-OBJECT rule head(S) => substrString(S, 0, 1) requires lengthString(S) >Int 0 rule tail(S) => "" requires lengthString(S) <=Int 0 rule tail(S) => substrString(S, 1, lengthString(S)) requires lengthString(S) >Int 0 - + endmodule ``` diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md index 6a1dc64..6697246 100644 --- a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md +++ b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md @@ -1,11 +1,13 @@ ```k requires "integer.md" +requires "map.md" requires "symbol.md" requires "vector.md" module HOSTFUNS imports HOST-INTEGER + imports HOST-MAP imports HOST-SYMBOL imports HOST-VECTOR endmodule diff --git a/src/ksoroban/kdist/soroban-semantics/host/map.md b/src/ksoroban/kdist/soroban-semantics/host/map.md new file mode 100644 index 0000000..1f4fec8 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/host/map.md @@ -0,0 +1,147 @@ +# Map + +```k +requires "../configuration.md" +requires "../switch.md" +requires "../wasm-ops.md" +requires "integer.md" +requires "symbol.md" +requires "vector.md" + +module HOST-MAP + imports CONFIG-OPERATIONS + imports WASM-OPERATIONS + imports HOST-INTEGER + imports HOST-SYMBOL + imports HOST-VECTOR + imports SWITCH-SYNTAX +``` + +## map_unpack_to_linear_memory + +Writes values from a map (`ScMap`) to a specified memory address. +Given a map (`MAPOBJ`) and an array of byte slices (`KEYS_POS`) for keys, it retrieves corresponding values from the map +and writes them sequentially to the address (`VALS_POS`). + +```k + rule [hostfun-map-unpack-to-linear-memory]: + hostCall ( "m" , "a" , [ i64 i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VALS_POS)) + ~> loadObject(HostVal(MAPOBJ)) + ~> #memLoad(getMajor(HostVal(KEYS_POS)), 8 *Int getMajor(HostVal(LEN))) + ~> loadSlices + ~> mapUnpackToLinearMemory + ~> toSmall(Void) + ... + + + 0 |-> < i64 > MAPOBJ // ScMap + 1 |-> < i64 > KEYS_POS // U32 + 2 |-> < i64 > VALS_POS // U32 + 3 |-> < i64 > LEN // U32 + + requires fromSmallValid(HostVal(KEYS_POS)) + andBool fromSmallValid(HostVal(LEN)) + + syntax InternalInstr ::= "mapUnpackToLinearMemory" [symbol(mapUnpackToLinearMemory)] + // ----------------------------------------------------------------------------------------- + rule [mapUnpackToLinearMemory]: + mapUnpackToLinearMemory + => #memStore( + VALS_POS, + Vals2Bytes( + lookupMany(OBJS, KEYS, 0) + ) + ) + ... + + KEYS : ScMap(OBJS) : U32(VALS_POS) : S => S + +``` + +## map_new_from_linear_memory + +Creates a map (`ScMap`) from specified keys and values. +Given an array of byte slices (`KEYS_POS`) for keys and an array of values (`VALS_POS`), +it constructs a map where keys are `Symbol`s created from the byte slices. +The function returns a `HostVal` pointing to the new map object. + +```k + rule [hostfun-map-new-from-linear-memory]: + hostCall ( "m" , "9" , [ i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => #memLoad(getMajor(HostVal(VALS_POS)), 8 *Int getMajor(HostVal(LEN))) + ~> #memLoad(getMajor(HostVal(KEYS_POS)), 8 *Int getMajor(HostVal(LEN))) + ~> loadSlices + ~> mapNewFromLinearMemory + ... + + + 0 |-> < i64 > KEYS_POS // U32 + 1 |-> < i64 > VALS_POS // U32 + 2 |-> < i64 > LEN // U32 + + requires fromSmallValid(HostVal(KEYS_POS)) + andBool fromSmallValid(HostVal(LEN)) + + syntax InternalInstr ::= "mapNewFromLinearMemory" [symbol(mapNewFromLinearMemory)] + // ---------------------------------------------------------------------------------------- + rule [mapNewFromLinearMemory]: + mapNewFromLinearMemory + => allocObject( + ScMap( + mapFromLists( + KEYS, + Bytes2Vals(VALS_BS) + ) + ) + ) + ~> returnHostVal + ... + + KEYS : VALS_BS : S => S + requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8 + +``` + +## Helpers + + +```k + + syntax List ::= Bytes2U32List(Bytes) [function, total, symbol(Bytes2U32List)] + // -------------------------------------------------------------------------------- + rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned)) + Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS))) + requires lengthBytes(BS) >=Int 4 + rule Bytes2U32List(BS) => .List + requires lengthBytes(BS) loadSlices + => loadSlicesAux(Bytes2U32List(KEY_SLICES)) + ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8) + ... + + KEY_SLICES : S => S + + rule [loadSlicesAux-empty]: + loadSlicesAux(.List) => .K ... + + rule [loadSlicesAux]: + loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN)) + => #memLoad(OFFSET, LEN) + ~> mkSymbolFromStack + ~> loadSlicesAux(REST) + ... + + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/symbol.md b/src/ksoroban/kdist/soroban-semantics/host/symbol.md index 70932d5..61032ec 100644 --- a/src/ksoroban/kdist/soroban-semantics/host/symbol.md +++ b/src/ksoroban/kdist/soroban-semantics/host/symbol.md @@ -28,6 +28,7 @@ module HOST-SYMBOL syntax InternalInstr ::= "symbolNewFromLinearMemory" [symbol(symbolNewFromLinearMemory)] + // --------------------------------------------------------------------------------- rule [symbolNewFromLinearMemory]: symbolNewFromLinearMemory => allocObject(Symbol(Bytes2String(BS))) @@ -36,5 +37,12 @@ module HOST-SYMBOL BS:Bytes : S => S requires validSymbol(Bytes2String(BS)) + + syntax InternalInstr ::= "mkSymbolFromStack" [symbol(mkSymbolFromStack)] + // --------------------------------------------------------------------------------- + rule [mkSymbolFromStack]: + mkSymbolFromStack => .K ... + (BS => Symbol(Bytes2String(BS))) : _ + endmodule ``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md index d82dce3..8377e9f 100644 --- a/src/ksoroban/kdist/soroban-semantics/kasmer.md +++ b/src/ksoroban/kdist/soroban-semantics/kasmer.md @@ -45,7 +45,7 @@ module KASMER rule [load-program]: (_S:Step _SS:Steps) #as PGM => .Steps _ => PGM - + rule [steps-empty]: .Steps => .K .K @@ -75,7 +75,7 @@ module KASMER rule [setAccount-new]: setAccount(ADDR, BAL) => .K ... - ( .Bag => + ( .Bag => ADDR BAL @@ -125,7 +125,7 @@ module KASMER // ------------------------------------------------------------------------------------------------------- rule [callContractFromStack]: callContractFromStack(FROM, TO, FUNC) => callContract(FROM, TO, FUNC, ARGS) ... - ScVec(ARGS) : S => S + ARGS : S => S // -------------------------------------------------------------------------------------------------------------- rule [callTx]: diff --git a/src/tests/integration/data/structs.wast b/src/tests/integration/data/structs.wast new file mode 100644 index 0000000..66a2b11 --- /dev/null +++ b/src/tests/integration/data/structs.wast @@ -0,0 +1,425 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", + +;; #![no_std] +;; use soroban_sdk::{contract, contractimpl, contracttype, Env, Vec}; + +;; #[contract] +;; pub struct IncrementContract; + +;; #[contracttype] +;; #[derive(PartialEq, Eq, Debug)] +;; pub struct Point { +;; x: u128, +;; y: u128 +;; } + +;; #[contractimpl] +;; impl IncrementContract { +;; pub fn make_struct(_env: Env, x: u128, y: u128) -> Point { +;; Point { x, y } +;; } + +;; pub fn destruct(env: Env, p: Point) -> Vec { +;; Vec::from_array(&env, [p.x, p.y]) +;; } +;; } + +(module $soroban_increment_contract.wasm + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func (param i64) (result i64))) + (type (;2;) (func (param i64 i64 i64) (result i64))) + (type (;3;) (func (param i64 i64 i64 i64) (result i64))) + (type (;4;) (func (param i32 i64))) + (type (;5;) (func)) + (import "i" "3" (func $_ZN17soroban_env_guest5guest3int20obj_from_u128_pieces17h5d7cf2ad07a3899bE (type 0))) + (import "i" "5" (func $_ZN17soroban_env_guest5guest3int16obj_to_u128_hi6417h645b49e080dcfdf6E (type 1))) + (import "i" "4" (func $_ZN17soroban_env_guest5guest3int16obj_to_u128_lo6417h0c596faaeffbf363E (type 1))) + (import "m" "9" (func $_ZN17soroban_env_guest5guest3map26map_new_from_linear_memory17h905b0cda6fdc76f0E (type 2))) + (import "m" "a" (func $_ZN17soroban_env_guest5guest3map27map_unpack_to_linear_memory17hb44f5a6c36f14cf3E (type 3))) + (import "v" "g" (func $_ZN17soroban_env_guest5guest3vec26vec_new_from_linear_memory17h31f0f68089eaf9f9E (type 0))) + (func $_ZN104_$LT$soroban_env_common..val..Val$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$u128$GT$$GT$12try_from_val17h5c3a8408ff9f5a37E (type 0) (param i64 i64) (result i64) + block ;; label = @1 + local.get 0 + i64.const 72057594037927935 + i64.gt_u + local.get 1 + i64.const 0 + i64.ne + local.get 1 + i64.eqz + select + br_if 0 (;@1;) + local.get 0 + i64.const 8 + i64.shl + i64.const 10 + i64.or + return + end + local.get 1 + local.get 0 + call $_ZN17soroban_env_guest5guest3int20obj_from_u128_pieces17h5d7cf2ad07a3899bE) + (func $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E (type 4) (param i32 i64) + (local i32 i64) + block ;; label = @1 + block ;; label = @2 + block ;; label = @3 + local.get 1 + i32.wrap_i64 + i32.const 255 + i32.and + local.tee 2 + i32.const 68 + i32.eq + br_if 0 (;@3;) + local.get 2 + i32.const 10 + i32.ne + br_if 1 (;@2;) + i64.const 0 + local.set 3 + local.get 0 + i32.const 16 + i32.add + i64.const 0 + i64.store + local.get 0 + local.get 1 + i64.const 8 + i64.shr_u + i64.store offset=8 + br 2 (;@1;) + end + local.get 1 + call $_ZN17soroban_env_guest5guest3int16obj_to_u128_hi6417h645b49e080dcfdf6E + local.set 3 + local.get 1 + call $_ZN17soroban_env_guest5guest3int16obj_to_u128_lo6417h0c596faaeffbf363E + local.set 1 + local.get 0 + i32.const 16 + i32.add + local.get 3 + i64.store + local.get 0 + local.get 1 + i64.store offset=8 + i64.const 0 + local.set 3 + br 1 (;@1;) + end + local.get 0 + i64.const 34359740419 + i64.store offset=8 + i64.const 1 + local.set 3 + end + local.get 0 + local.get 3 + i64.store) + (func $make_struct (type 0) (param i64 i64) (result i64) + (local i32 i32 i64 i64) + global.get $__stack_pointer + i32.const 32 + i32.sub + local.tee 2 + global.set $__stack_pointer + local.get 2 + i32.const 8 + i32.add + local.get 0 + call $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E + block ;; label = @1 + local.get 2 + i64.load offset=8 + i64.eqz + i32.eqz + br_if 0 (;@1;) + local.get 2 + i32.const 24 + i32.add + local.tee 3 + i64.load + local.set 0 + local.get 2 + i64.load offset=16 + local.set 4 + local.get 2 + i32.const 8 + i32.add + local.get 1 + call $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E + local.get 2 + i64.load offset=8 + i64.eqz + i32.eqz + br_if 0 (;@1;) + local.get 3 + i64.load + local.set 1 + local.get 2 + i64.load offset=16 + local.set 5 + local.get 4 + local.get 0 + call $_ZN104_$LT$soroban_env_common..val..Val$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$u128$GT$$GT$12try_from_val17h5c3a8408ff9f5a37E + local.set 0 + local.get 2 + local.get 5 + local.get 1 + call $_ZN104_$LT$soroban_env_common..val..Val$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$u128$GT$$GT$12try_from_val17h5c3a8408ff9f5a37E + i64.store offset=16 + local.get 2 + local.get 0 + i64.store offset=8 + i32.const 1048580 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + local.get 2 + i32.const 8 + i32.add + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.const 8589934596 + call $_ZN17soroban_env_guest5guest3map26map_new_from_linear_memory17h905b0cda6fdc76f0E + local.set 0 + local.get 2 + i32.const 32 + i32.add + global.set $__stack_pointer + local.get 0 + return + end + unreachable + unreachable) + (func $destruct (type 1) (param i64) (result i64) + (local i32 i32 i64 i64 i64 i32) + global.get $__stack_pointer + i32.const 48 + i32.sub + local.tee 1 + global.set $__stack_pointer + i32.const 0 + local.set 2 + block ;; label = @1 + loop ;; label = @2 + local.get 2 + i32.const 16 + i32.eq + br_if 1 (;@1;) + local.get 1 + i32.const 32 + i32.add + local.get 2 + i32.add + i64.const 2 + i64.store + local.get 2 + i32.const 8 + i32.add + local.set 2 + br 0 (;@2;) + end + end + block ;; label = @1 + local.get 0 + i64.const 255 + i64.and + i64.const 76 + i64.ne + br_if 0 (;@1;) + local.get 0 + i32.const 1048580 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + local.get 1 + i32.const 32 + i32.add + i64.extend_i32_u + local.tee 3 + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.const 8589934596 + call $_ZN17soroban_env_guest5guest3map27map_unpack_to_linear_memory17hb44f5a6c36f14cf3E + drop + local.get 1 + local.get 1 + i64.load offset=32 + call $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E + local.get 1 + i64.load + i64.eqz + i32.eqz + br_if 0 (;@1;) + local.get 1 + i32.const 16 + i32.add + local.tee 2 + i64.load + local.set 0 + local.get 1 + i64.load offset=8 + local.set 4 + local.get 1 + local.get 1 + i64.load offset=40 + call $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E + local.get 1 + i64.load + i64.eqz + i32.eqz + br_if 0 (;@1;) + local.get 1 + i64.load offset=8 + local.set 5 + local.get 1 + i32.const 24 + i32.add + local.get 2 + i64.load + i64.store + local.get 1 + local.get 5 + i64.store offset=16 + local.get 1 + local.get 4 + i64.store + local.get 1 + local.get 0 + i64.store offset=8 + i32.const 0 + local.set 2 + loop ;; label = @2 + block ;; label = @3 + local.get 2 + i32.const 16 + i32.ne + br_if 0 (;@3;) + i32.const 0 + local.set 2 + local.get 1 + local.set 6 + block ;; label = @4 + loop ;; label = @5 + local.get 2 + i32.const 16 + i32.eq + br_if 1 (;@4;) + local.get 1 + i32.const 32 + i32.add + local.get 2 + i32.add + local.get 6 + i64.load + local.get 6 + i32.const 8 + i32.add + i64.load + call $_ZN104_$LT$soroban_env_common..val..Val$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$u128$GT$$GT$12try_from_val17h5c3a8408ff9f5a37E + i64.store + local.get 6 + i32.const 16 + i32.add + local.set 6 + local.get 2 + i32.const 8 + i32.add + local.set 2 + br 0 (;@5;) + end + end + local.get 3 + i64.const 32 + i64.shl + i64.const 4 + i64.or + i64.const 8589934596 + call $_ZN17soroban_env_guest5guest3vec26vec_new_from_linear_memory17h31f0f68089eaf9f9E + local.set 0 + local.get 1 + i32.const 48 + i32.add + global.set $__stack_pointer + local.get 0 + return + end + local.get 1 + i32.const 32 + i32.add + local.get 2 + i32.add + i64.const 2 + i64.store + local.get 2 + i32.const 8 + i32.add + local.set 2 + br 0 (;@2;) + end + end + unreachable + unreachable) + (func $_ (type 5)) + (memory (;0;) 17) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048596)) + (global (;2;) i32 (i32.const 1048608)) + (export "memory" (memory 0)) + (export "make_struct" (func $make_struct)) + (export "destruct" (func $destruct)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2)) + (data $.rodata (i32.const 1048576) "xy\00\00\00\00\10\00\01\00\00\00\01\00\10\00\01\00\00\00")) + +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-ctr"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-ctr"), + "destruct", + ListItem( + ScMap( + Symbol(str("x")) |-> U128(111111111111111111) + Symbol(str("y")) |-> U128(222222222222222222) + ) + ), + ScVec(ListItem(U128(111111111111111111)) ListItem(U128(222222222222222222))) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-ctr"), + "make_struct", + ListItem(U128(111111111111111111)) ListItem(U128(222222222222222222)), + ScMap( + Symbol(str("x")) |-> U128(111111111111111111) + Symbol(str("y")) |-> U128(222222222222222222) + ) +) + +setExitCode(0) \ No newline at end of file