diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index ed581bb..9aa33ee 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -127,6 +127,15 @@ module CONFIG-OPERATIONS dropStack => .K ... _V : S => S + // Allows using `pushStack` and `dropStack` in the `` cell + rule [pushStack-instr]: + pushStack(V) => .K ... + S => V : S + + rule [dropStack-instr]: + dropStack => .K ... + _V : S => S + ``` ## Call State diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index 1df7297..036651b 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -196,12 +196,18 @@ module HOST-OBJECT syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal [function, total, symbol(HostVal:getOrDefault)] // --------------------------------------------------------- - rule OBJS {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D) + rule OBJS:List {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D) requires 0 <=Int I andBool I D + rule _OBJS:List {{ _I }} orDefault (D:HostVal) => D [owise] + // typed version of builtin MAP [ K ] orDefault V + syntax HostVal ::= Map "{{" KItem "}}" "orDefault" HostVal + [function, total, symbol(HostVal:lookupOrDefault)] + // --------------------------------------------------------- + rule OBJS:Map {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ] orDefault D, D) + ``` ## Conversion between `HostVal` and `ScVal` diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md index 9e6adfd..acb4500 100644 --- a/src/komet/kdist/soroban-semantics/host/map.md +++ b/src/komet/kdist/soroban-semantics/host/map.md @@ -17,6 +17,136 @@ module HOST-MAP imports SWITCH-SYNTAX ``` +## map_new + +```k + rule [hostfun-map-new]: + hostCall ( "m" , "_" , [ .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject(ScMap(.Map)) + ~> returnHostVal + ... + + .Map +``` + +## map_put + +```k + rule [hostfun-map-put]: + hostCall ( "m" , "0" , [ i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => pushStack(HostVal(VAL)) + ~> loadObjectFull(HostVal(KEY)) + ~> loadObject(HostVal(M)) + ~> hostCallAux("m", "0") + ... + + + 0 |-> < i64 > M + 1 |-> < i64 > KEY + 2 |-> < i64 > VAL + + + rule [hostCallAux-map-put]: + hostCallAux("m", "0") + => allocObject(ScMap( M [ KEY <- VAL ] )) + ~> returnHostVal + ... + + ScMap(M) : KEY:ScVal : VAL:HostVal : S => S + +``` + +## map_get + +```k + rule [hostfun-map-get]: + hostCall ( "m" , "1" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObjectFull(HostVal(KEY)) + ~> loadObject(HostVal(M)) + ~> hostCallAux("m", "1") + ... + + + 0 |-> < i64 > M + 1 |-> < i64 > KEY + + + rule [hostCallAux-map-get]: + hostCallAux("m", "1") + => pushStack( M {{ KEY }} orDefault HostVal(-1) ) + ~> returnHostVal + ... + + ScMap(M) : KEY:ScVal : S => S + requires KEY in_keys(M) + + rule [hostCallAux-map-get-not-found]: + hostCallAux("m", "1") => trap ... + ScMap(M) : KEY:ScVal : S => S + requires notBool( KEY in_keys(M) ) + +``` + +## map_del + +```k + rule [hostfun-map-del]: + hostCall ( "m" , "2" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObjectFull(HostVal(KEY)) + ~> loadObject(HostVal(M)) + ~> hostCallAux("m", "2") + ... + + + 0 |-> < i64 > M + 1 |-> < i64 > KEY + + + rule [hostCallAux-map-del]: + hostCallAux("m", "2") + => allocObject(ScMap( M [ KEY <- undef ] )) + ~> returnHostVal + ... + + ScMap(M) : KEY:ScVal : S => S + requires KEY in_keys(M) + + rule [hostCallAux-map-del-not-found]: + hostCallAux("m", "2") => trap ... + ScMap(M) : KEY:ScVal : S => S + requires notBool( KEY in_keys(M) ) + +``` + +## map_len + +```k + rule [hostCallAux-map-len]: + hostCallAux("m", "3") => toSmall(U32(size(M))) ... + ScMap(M) : S => S +``` + +## map_has + +```k + rule [hostfun-map-has]: + hostCall ( "m" , "4" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObjectFull(HostVal(KEY)) + ~> loadObject(HostVal(M)) + ~> hostCallAux("m", "4") + ... + + + 0 |-> < i64 > M + 1 |-> < i64 > KEY + + + rule [hostCallAux-map-has]: + hostCallAux("m", "4") => toSmall(SCBool( KEY in_keys(M) )) ... + ScMap(M) : KEY:ScVal : S => S + +``` + ## map_unpack_to_linear_memory Writes values from a map (`ScMap`) to a specified memory address. diff --git a/src/komet/kdist/soroban-semantics/wasm-ops.md b/src/komet/kdist/soroban-semantics/wasm-ops.md index c5101c3..febf66c 100644 --- a/src/komet/kdist/soroban-semantics/wasm-ops.md +++ b/src/komet/kdist/soroban-semantics/wasm-ops.md @@ -62,6 +62,42 @@ module WASM-OPERATIONS [owise] ``` +## Host function operations + +- `hostCallAux(MOD,FUNC)`: Helper instruction for implementing host functions with arguments already loaded onto the + host stack. Reduces the need to define custom `InternalInstr` productions for each host function. + The `hostCall-default` rule provides default behavior for host functions without complex argument handling, allowing + `hostCallAux` to streamline the process further. +- `loadArgs(N)`: Loads the first `N` arguments onto the host stack using `loadObject` starting from the last argument. + This positions the first argument at the top of the stack at the end. + +```k + syntax InternalInstr ::= hostCallAux(String, String) [symbol(hostCallAux)] + | loadArgs(Int) [symbol(loadArgs)] + + // Default implementation for `hostCall`. Loads the arguments to the host stack using `loadObject` + rule [hostCall-default]: + hostCall(MOD, FUNC, [ _ARGS ] -> [ _RET ]) + => loadArgs(size(LOCALS)) + ~> hostCallAux(MOD, FUNC) + ... + + LOCALS + [owise] + + rule [loadArgs-empty]: + loadArgs(0) => .K ... + + rule [loadArgs]: + loadArgs(I) + => loadObject(HostVal(X)) + ~> loadArgs(I -Int 1) + ... + + ... (I -Int 1) |-> X ... + +``` + ```k endmodule -``` \ No newline at end of file +``` diff --git a/src/tests/integration/data/map.wast b/src/tests/integration/data/map.wast new file mode 100644 index 0000000..29d3842 --- /dev/null +++ b/src/tests/integration/data/map.wast @@ -0,0 +1,191 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module + (import "m" "_" (func $new (result i64))) + (import "m" "0" (func $put (param i64 i64 i64) (result i64))) + (import "m" "1" (func $get (param i64 i64) (result i64))) + (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))) + + (export "new" (func $new)) + (export "put" (func $put)) + (export "get" (func $get)) + (export "del" (func $del)) + (export "len" (func $len)) + (export "has" (func $has)) +) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; map_new +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "new", + .List, + ScMap(.Map) +) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; map_has +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "has", + ListItem(ScMap(.Map)) ListItem(Symbol(str("foo"))), + SCBool(false) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "has", + ListItem(ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )) + ListItem(Symbol(str("foo"))), + SCBool(true) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "has", + ListItem(ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )) + ListItem(Symbol(str("qux"))), + SCBool(false) +) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; map_len +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "len", + ListItem(ScMap(.Map)), + U32(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "len", + ListItem(ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )), + U32(3) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; map_get +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "get", + ListItem(ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )) + ListItem(Symbol(str("foo"))), + U32(123) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; map_del +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "del", + ListItem(ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )) + ListItem(Symbol(str("foo"))), + ScMap( + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + ) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; map_put +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "put", + ListItem(ScMap(.Map)) ListItem(Symbol(str("foo"))) ListItem(U32(123456)), + ScMap(Symbol(str("foo")) |-> U32(123456)) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "put", + ListItem(ScMap( + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )) + ListItem(Symbol(str("foo"))) + ListItem(U32(123)), + ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + ) +) + +;; Overwrite +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "put", + ListItem(ScMap( + Symbol(str("foo")) |-> U32(1) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + )) + ListItem(Symbol(str("foo"))) + ListItem(U32(123)), + ScMap( + Symbol(str("foo")) |-> U32(123) + Symbol(str("bar")) |-> Symbol(str("456")) + Symbol(str("baz")) |-> U128(789) + ) +) + +setExitCode(0) \ No newline at end of file