diff --git a/package/version b/package/version index 9faa1b7..c946ee6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.5 +0.1.6 diff --git a/pyproject.toml b/pyproject.toml index 6a0f92a..2bff047 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,12 +4,15 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.5" +version = "0.1.6" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", ] +[tool.poetry.scripts] +ksoroban = "ksoroban.ksoroban:main" + [tool.poetry.plugins.kdist] soroban-semantics = "ksoroban.kdist.plugin" diff --git a/src/ksoroban/kdist/plugin.py b/src/ksoroban/kdist/plugin.py index d8b1346..0e68f3f 100644 --- a/src/ksoroban/kdist/plugin.py +++ b/src/ksoroban/kdist/plugin.py @@ -48,8 +48,8 @@ def deps(self) -> tuple[str]: 'source': SourceTarget(), 'llvm': KompileTarget( lambda src_dir: { - 'main_file': src_dir / 'soroban-semantics/soroban.md', - 'syntax_module': 'SOROBAN', + 'main_file': src_dir / 'soroban-semantics/kasmer.md', + 'syntax_module': 'KASMER-SYNTAX', 'include_dirs': [src_dir], 'md_selector': 'k', 'warnings_to_errors': True, diff --git a/src/ksoroban/kdist/soroban-semantics/auto-allocate.md b/src/ksoroban/kdist/soroban-semantics/auto-allocate.md new file mode 100644 index 0000000..df6f126 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/auto-allocate.md @@ -0,0 +1,84 @@ +Auto Allocate Host Modules +========================== + +When `AUTO-ALLOCATE` is imported, an new module will be automatically created and registered whenever necessary to resolve an import. +This makes it possible to implement host modules easily in K. +Accessing the import will result in an instruction being left on the `instrs` cell that can't be resolved in the regular Wasm semantics. +Instead, the embedder can add rules for handling the host import. + +Currently, only function imports are supported. +Calling an imported host function will result in `hostCall(MODULE_NAME, FUNCTION_NAME, FUNCTION_TYPE)` being left on the `instrs` cell. + +```k +requires "wasm-semantics/wasm-text.md" + +module WASM-AUTO-ALLOCATE + imports WASM-DATA-TOOLS + imports WASM-TEXT + + syntax Stmt ::= "newEmptyModule" WasmString + // ------------------------------------------- + rule newEmptyModule MODNAME => .K ... + MR => MR [ MODNAME <- NEXT ] + NEXT => NEXT +Int 1 + ( .Bag => NEXT ... ) ... + + syntax Stmts ::= autoAllocModules ( ModuleDecl, Map ) [function] + | #autoAllocModules ( Defns , Map ) [function] + // ----------------------------------------------------------------- + rule autoAllocModules(#module(... importDefns:IS), MR) => #autoAllocModules(IS, MR) +``` + +In helper function `#autoAllocModules`, the module registry map is passed along to check if the module being imported from is present. +It is treated purely as a key set -- the actual stored values are not used or stored anywhere. + +```k + rule #autoAllocModules(.Defns, _) => .Stmts + rule #autoAllocModules((#import(MOD, _, _) DS) => DS, MR) requires MOD in_keys(MR) + rule #autoAllocModules((#import(MOD, _, _) DS), MR) + => newEmptyModule MOD #autoAllocModules(DS, MR [MOD <- -1]) + requires notBool MOD in_keys(MR) + + rule MD:ModuleDecl + => sequenceStmts(autoAllocModules(MD, MR)) + ~> MD + ... + + MR + requires autoAllocModules(MD, MR) =/=K .Stmts + [priority(10)] + + syntax Instr ::= hostCall(String, String, FuncType) + // --------------------------------------------------- + rule (.K => allocfunc(HOSTMOD, NEXTADDR, TYPE, [ .ValTypes ], hostCall(wasmString2StringStripped(MOD), wasmString2StringStripped(NAME), TYPE) .Instrs, #meta(... id: String2Identifier("$auto-alloc:" +String #parseWasmString(MOD) +String ":" +String #parseWasmString(NAME) ), localIds: .Map ))) + ~> #import(MOD, NAME, #funcDesc(... type: TIDX)) + ... + + CUR + + CUR + ... TIDX |-> TYPE ... + ... + + NEXTADDR => NEXTADDR +Int 1 + ... MOD |-> HOSTMOD ... + + HOSTMOD + EXPORTS => EXPORTS [NAME <- NEXTFUNC ] + FS => setExtend(FS, NEXTFUNC, NEXTADDR, -1) + NEXTFUNC => NEXTFUNC +Int 1 + NEXTTYPE => NEXTTYPE +Int 1 + TYPES => TYPES [ NEXTTYPE <- TYPE ] + ... + + requires notBool NAME in_keys(EXPORTS) + + syntax String ::= wasmString2StringStripped ( WasmString ) [function] + | #stripQuotes ( String ) [function] + // ---------------------------------------------------- + rule wasmString2StringStripped(WS) => #stripQuotes(#parseWasmString(WS)) + + rule #stripQuotes(S) => replaceAll(S, "\"", "") + +endmodule +``` diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md new file mode 100644 index 0000000..620aaa1 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/configuration.md @@ -0,0 +1,268 @@ + +```k +requires "auto-allocate.md" +requires "wasm-semantics/wasm.md" +requires "data.md" + +module CONFIG + imports HOST-OBJECT + imports MAP + imports WASM + + configuration + + .K + + + Contract(.Bytes) + Account(.Bytes) + .WasmString + .List + + .List // List of HostVals with absolute handles to host objects + .Int + + .HostStack + .List // List of ScVals + .List + .List + + + + + Contract(.Bytes) + .Bytes + .Map + + + + + Account(.Bytes) + 0 + + + .Map + .List + + + syntax HostStack ::= List{HostStackVal, ":"} [symbol(hostStackList)] + syntax HostStackVal ::= ScVal | HostVal + + + syntax InternalCmd ::= #callResult(ValStack, List) [symbol(#callResult)] + +endmodule +``` + + +```k +module CONFIG-OPERATIONS + imports WASM-AUTO-ALLOCATE + imports CONFIG + imports SWITCH-SYNTAX +``` + +## Stack operations + +```k + syntax InternalCmd ::= pushStack(HostStackVal) [symbol(pushStack)] + // --------------------------------------------------------------------- + rule [pushStack]: + pushStack(V) => .K ... + S => V : S + + syntax InternalCmd ::= "dropStack" [symbol(dropStack)] + // --------------------------------------------------------------------- + rule [dropStack]: + dropStack => .K ... + _V : S => S + +``` + +## Call State + +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 + syntax InternalCmd ::= "pushCallState" [symbol(pushCallState)] + // --------------------------------------- + rule [pushCallState]: + pushCallState => .K ... + (.List => ListItem(CALLSTATE)) ... + CALLSTATE:CallStateCell + [priority(60)] + + syntax InternalCmd ::= "popCallState" [symbol(popCallState)] + // -------------------------------------- + rule [popCallState]: + popCallState => .K ... + (ListItem(CALLSTATE:CallStateCell) => .List) ... + (_:CallStateCell => CALLSTATE) + [priority(60)] + + syntax InternalCmd ::= "dropCallState" [symbol(dropCallState)] + // --------------------------------------- + rule [dropCallState]: + dropCallState => .K ... + (ListItem(_) => .List) ... + [priority(60)] + + syntax InternalCmd ::= "resetCallstate" [symbol(resetCallState)] + // --------------------------------------------------------------------------- + rule [resetCallstate]: + resetCallstate => .K ... + (_:CallStateCell => .K ... ) + [preserves-definedness] // all constant configuration cells should be defined + +``` + +## World State + +```k + syntax AccountsCellFragment + syntax ContractsCellFragment + + syntax Accounts ::= "{" AccountsCellFragment "," ContractsCellFragment "}" + // -------------------------------------------------------- + + syntax InternalCmd ::= "pushWorldState" [symbol(pushWorldState)] + // --------------------------------------- + rule [pushWorldState]: + pushWorldState => .K ... + (.List => ListItem({ ACCTDATA , CONTRACTS })) ... + CONTRACTS + ACCTDATA + [priority(60)] + + syntax InternalCmd ::= "popWorldState" [symbol(popWorldState)] + // -------------------------------------- + rule [popWorldState]: + popWorldState => .K ... + (ListItem({ ACCTDATA , CONTRACTS }) => .List) ... + _ => CONTRACTS + _ => ACCTDATA + [priority(60)] + + syntax InternalCmd ::= "dropWorldState" [symbol(dropWorldState)] + // --------------------------------------- + rule [dropWorldState]: + dropWorldState => .K ... + (ListItem(_) => .List) ... + [priority(60)] +``` + +## `ScVal` Operations + +```k + syntax InternalCmd ::= allocObject(ScVal) [symbol(allocObject)] + // --------------------------------------------------------------------------- + rule [allocObject-small]: + allocObject(SCV) => .K ... + STACK => toSmall(SCV) : STACK + requires toSmallValid(SCV) + + rule [allocObject]: + allocObject(SCV) => .K ... + OBJS => OBJS ListItem(SCV) + STACK => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK + [owise] + + syntax InternalCmd ::= allocObjects (List) [symbol(allocObjects)] + | allocObjectsAux (List) [symbol(allocObjectsAux)] + | allocObjectsCollect(Int) [symbol(allocObjectsCollect)] + // --------------------------------------------------------------------------- + rule [allocObjects]: + allocObjects(L) => allocObjectsAux(L) ~> allocObjectsCollect(size(L)) ... + + rule [allocObjectsAux-empty]: + allocObjectsAux(.List) => .K ... + + rule [allocObjectsAux]: + allocObjectsAux(ListItem(SCV:ScVal) L) + => allocObjectsAux(L) + ~> allocObject(SCV) + ... + + + rule [allocObjectsCollect]: + allocObjectsCollect(LENGTH) => .K ... + STACK => ScVec(take(LENGTH, STACK)) : drop(LENGTH, STACK) + + syntax HostStack ::= drop(Int, HostStack) [function, total, symbol(HostStack:drop)] + // ------------------------------------------------------------------------------------- + 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] + + syntax InternalInstr ::= loadObject(HostVal) [symbol(loadObject)] + // -------------------------------------------------------------------- + rule [loadObject-abs]: + loadObject(VAL) => .K ... + S => OBJS {{ getIndex(VAL) }} orDefault Void : S + OBJS + requires isObject(VAL) + andBool notBool isRelativeObjectHandle(VAL) + andBool 0 <=Int getIndex(VAL) + andBool getIndex(VAL) loadObject(VAL) + => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0)) + ... + + RELS + requires isObject(VAL) + andBool isRelativeObjectHandle(VAL) + andBool 0 <=Int getIndex(VAL) + andBool getIndex(VAL) #callResult(.ValStack, _RELS) => .K ... + + rule [callResult]: + #callResult( I : SS, RELS) + => #callResult(SS, RELS) + ~> HostVal2ScVal(HostVal(I), RELS) + ... + + + syntax InternalCmd ::= HostVal2ScVal(HostVal, List) [symbol(HostVal2ScVal)] + // -------------------------------------------------------------------------- + rule [HostVal2ScVal-obj-abs]: + HostVal2ScVal(VAL, _RELS) => .K ... + OBJS + S => OBJS {{ getIndex(VAL) }} orDefault Void : S + requires isObject(VAL) + andBool notBool(isRelativeObjectHandle(VAL)) + andBool getIndex(VAL) HostVal2ScVal(VAL, RELS) + => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), RELS) + ... + + requires isObject(VAL) + andBool isRelativeObjectHandle(VAL) + andBool getIndex(VAL) HostVal2ScVal(VAL, _RELS) => .K ... + S => fromSmall(VAL) : S + requires notBool isObject(VAL) + andBool fromSmallValid(VAL) + +``` + +```k +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/data.md b/src/ksoroban/kdist/soroban-semantics/data.md new file mode 100644 index 0000000..e876155 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/data.md @@ -0,0 +1,209 @@ + +[Documentation - Host Value Type](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type) + +```k +module HOST-OBJECT-SYNTAX + imports BOOL-SYNTAX + imports INT-SYNTAX + imports BYTES-SYNTAX + imports STRING-SYNTAX + imports LIST + imports MAP +``` + +## ScVal + +[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. + + +```k + syntax ScVal + ::= SCBool(Bool) [symbol(SCVal:Bool)] + | "Void" [symbol(SCVal:Void)] + | U32(Int) [symbol(SCVal:U32)] + | I32(Int) [symbol(SCVal:I32)] + | U64(Int) [symbol(SCVal:U64)] + | I64(Int) [symbol(SCVal:I64)] + | ScVec(List) [symbol(SCVal:Vec)] + | ScMap(Map) [symbol(SCVal:Map)] + | ScAddress(Address) [symbol(SCVal:Address)] + + syntax Address ::= AccountId | ContractId + syntax AccountId ::= Account(Bytes) [symbol(AccountId)] + syntax ContractId ::= Contract(Bytes) [symbol(ContractId)] + +``` + +## HostVal + +[Documentation: HostVal](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type) + +`HostVal` is used to pass values to and from Wasm contracts. It is a 64-bit representation of `ScVal`. + +Bit-packed Representation: + + * Tag (Low 8 bits): The lower 8 bits make up the tag. The tag value determines how the remaining 56 bits are to be interpreted. + * Body (High 56 bits): The body can be split into two parts: + * Minor Component (Low 24 bits): The lower 24 bits of the body. + * Major Component (High 32 bits): The upper 32 bits of the body. + +Some HostVal instances, known as small values, are self-contained and carry all the information necessary to convert them to ScVal. Other HostVal instances contain a handle in their major component to a ScVal stored on the host side. + +```k + syntax HostVal ::= HostVal(Int) [symbol(HostVal)] + +endmodule + +module HOST-OBJECT + imports INT + imports BOOL + imports LIST + imports MAP + imports STRING + imports BYTES + imports HOST-OBJECT-SYNTAX + imports WASM + + syntax Int ::= getMajor(HostVal) [function, total, symbol(getMajor)] + | getTag(HostVal) [function, total, symbol(getTag)] + | getBody(HostVal) [function, total, symbol(getBody)] + // ----------------------------------------------------------------------- + rule getMajor(HostVal(I)) => I >>Int 32 + rule getTag(HostVal(I)) => I &Int 255 + rule getBody(HostVal(I)) => I >>Int 8 + + syntax Bool ::= isObject(HostVal) [function, total, symbol(isObject)] + | 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 isRelativeObjectHandle(V) => getMajor(V) &Int 1 ==Int 0 + + syntax Int ::= indexToHandle(Int, Bool) [function, total, symbol(indexToHandle)] + // -------------------------------------------------------------------------------- + rule indexToHandle(I, false) => (I < I < 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)] + // -------------------------------------------------------------------------------- + rule fromHandleAndTag(H, T) => fromMajorMinorAndTag(H, 0, T) + rule fromMajorMinorAndTag(MAJ, MIN, TAG) => fromBodyAndTag((MAJ < HostVal((BODY < #unparseWasmString("\"" +String S +String "\"") + + // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values + syntax Int ::= getTag(ScVal) [function, total] + // ----------------------------------------------------- + rule getTag(SCBool(true)) => 0 + rule getTag(SCBool(false)) => 1 + rule getTag(Void) => 2 + 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 ) + rule getTag(I64(_)) => 65 // I64small is not implemented + rule getTag(ScVec(_)) => 75 + rule getTag(ScMap(_)) => 76 + rule getTag(ScAddress(_)) => 77 + + // 64-bit integers that fit in 56 bits + syntax Int ::= "#maxU64small" [macro] + | "#maxI64small" [macro] + | "#minI64small" [macro] + // ----------------------------------------- + rule #maxU64small => 72057594037927935 + rule #maxI64small => 36028797018963967 + rule #minI64small => -36028797018963968 + + syntax ScVal ::= ScValOrDefault(KItem, ScVal) [function, total, symbol(ScValOrDefault)] + // --------------------------------------------------------- + rule ScValOrDefault(X:ScVal, _:ScVal) => X + rule ScValOrDefault(_, D:ScVal) => D [owise] + + syntax HostVal ::= HostValOrDefault(KItem, HostVal) [function, total, symbol(HostValOrDefault)] + // --------------------------------------------------------- + rule HostValOrDefault(X:HostVal, _:HostVal) => X + rule HostValOrDefault(_, D:HostVal) => D [owise] + + syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal + [function, total, symbol(List:getOrDefault)] + // --------------------------------------------------------- + rule OBJS {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ], D) + requires 0 <=Int I andBool I D + [owise] + + syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal + [function, total, symbol(HostVal:getOrDefault)] + // --------------------------------------------------------- + rule OBJS {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D) + requires 0 <=Int I andBool I D + [owise] + +``` + +## Conversion between `HostVal` and `ScVal` + + +```k + syntax ScVal ::= fromSmall(HostVal) [function, total, symbol(fromSmall)] + // ----------------------------------------------------------------------------------- + rule fromSmall(VAL) => SCBool(false) requires getTag(VAL) ==Int 0 + + rule fromSmall(VAL) => SCBool(true) requires getTag(VAL) ==Int 1 + + rule fromSmall(VAL) => Void requires getTag(VAL) ==Int 2 + + rule fromSmall(VAL) => U32(getMajor(VAL)) requires getTag(VAL) ==Int 4 + + rule fromSmall(VAL) => I32(#signed(i32, getMajor(VAL))) + requires getTag(VAL) ==Int 5 + andBool definedSigned(i32, getMajor(VAL)) + [preserves-definedness] + + rule fromSmall(VAL) => U64(getBody(VAL)) requires getTag(VAL) ==Int 6 + + // return `Void` for invalid values + rule fromSmall(_) => Void [owise] + + syntax Bool ::= fromSmallValid(HostVal) + [function, total, symbol(fromSmallValid)] + // --------------------------------------------------------------------------------- + rule fromSmallValid(VAL) => fromSmall(VAL) =/=K Void orBool getTag(VAL) ==Int 2 + + + syntax HostVal ::= toSmall(ScVal) [function, total, symbol(toSmall)] + // --------------------------------------------------------------------------------- + rule toSmall(SCBool(false)) => fromMajorMinorAndTag(0, 0, 0) + rule toSmall(SCBool(true)) => fromMajorMinorAndTag(0, 0, 1) + rule toSmall(Void) => fromMajorMinorAndTag(0, 0, 2) + rule toSmall(U32(I)) => fromMajorMinorAndTag(I, 0, 4) + rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5) + requires definedUnsigned(i32, I) + rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small + rule toSmall(_) => HostVal(-1) [owise] + + syntax Bool ::= toSmallValid(ScVal) + [function, total, symbol(toSmallValid)] + // --------------------------------------------------------------------------------- + rule toSmallValid(VAL) => toSmall(VAL) =/=K HostVal(-1) + + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md new file mode 100644 index 0000000..c4512cd --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md @@ -0,0 +1,8 @@ + +```k +requires "integer.md" + +module HOSTFUNS + imports HOST-INTEGER +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/integer.md b/src/ksoroban/kdist/soroban-semantics/host/integer.md new file mode 100644 index 0000000..5db9c6c --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/host/integer.md @@ -0,0 +1,57 @@ + +```k +requires "../configuration.md" + +module HOST-INTEGER + imports CONFIG-OPERATIONS + + syntax InternalInstr ::= "returnU64" [symbol(returnU64)] + | "returnI64" [symbol(returnI64)] + | "returnHostVal" [symbol(returnHostVal)] + // ------------------------------------------------------------ + rule [returnU64]: + returnU64 => i64.const I ... + U64(I) : S => S + + rule [returnI64]: + returnI64 => i64.const #unsigned(i64, I) ... + I64(I) : S => S + requires definedUnsigned(i64, I) + [preserves-definedness] + + rule [returnHostVal]: + returnHostVal => i64.const I ... + HostVal(I) : S => S + + rule [hostfun-obj-to-u64]: + hostCall ( "i" , "0" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VAL)) + ~> returnU64 + ... + + + 0 |-> < i64 > VAL + + + rule [hostfun-obj-from-u64]: + hostCall ( "i" , "_" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => #waitCommands + ~> returnHostVal + ... + + + 0 |-> < i64 > I + + (.K => allocObject(U64(I))) ... + + rule [hostfun-obj-to-i64]: + hostCall ( "i" , "2" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VAL)) + ~> returnI64 + ... + + + 0 |-> < i64 > VAL + +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 new file mode 100644 index 0000000..7c965d3 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/kasmer.md @@ -0,0 +1,150 @@ + +```k +requires "soroban.md" + +module KASMER-SYNTAX + imports WASM-TEXT-SYNTAX + imports WASM-TEXT-COMMON-SYNTAX + imports KASMER-SYNTAX-COMMON +endmodule + +module KASMER-SYNTAX-COMMON + // imports WASM + imports HOST-OBJECT-SYNTAX + + syntax ModuleDecl + syntax WasmString + + syntax Step ::= setExitCode(Int) [symbol(setExitCode)] + | setAccount( address: AccountId, balance: Int) [symbol(setAccount)] + | uploadWasm(Bytes, ModuleDecl) [symbol(uploadWasm)] + | deployContract( from: Address, address: ContractId, wasmHash: Bytes, args: List ) [symbol(deployContract)] + | callTx( from: Address, to: Address, func: WasmString, args: List, result: ScVal) [symbol(callTx)] + + + syntax Steps ::= List{Step, ""} [symbol(kasmerSteps)] + +endmodule + +module KASMER + imports SOROBAN + imports KASMER-SYNTAX-COMMON + + configuration + + $PGM:Steps + + 1 + + + rule [load-program]: + (_S:Step _SS:Steps) #as PGM => .Steps + _ => PGM + + rule [steps-empty]: + .Steps => .K + .K + + rule [steps-seq]: + S:Step SS:Steps => S ~> SS ... + .K + + syntax Step ::= "#hostTrap" [symbol(#hostTrap)] + + // -------------------------------------------------------- + rule [setExitCode]: + setExitCode(I) => .K ... + _ => I + .K + + + // ----------------------------------------------------------------------------------- + rule [setAccount-existing]: + setAccount(ADDR, BAL) => .K ... + + ADDR + _ => BAL + ... + + [priority(50)] + + rule [setAccount-new]: + setAccount(ADDR, BAL) => .K ... + ( .Bag => + + ADDR + BAL + + ) + [priority(55)] + +// ---------------------------------------------------------------------------- + rule [uploadWasm]: + uploadWasm(HASH, MOD) => .K ... + MODS => MODS [ HASH <- MOD ] + requires notBool( HASH in_keys(MODS) ) + + rule [uploadWasm-exists]: + uploadWasm(HASH, _MOD) => .K ... + MODS + requires HASH in_keys(MODS) + + // ----------------------------------------------------------------------------------------------------------------------- + rule [deployContract-existing]: + deployContract(_OWNER, ADDR, _WASM_HASH, _ARGS) => #hostTrap ... + + ADDR + ... + + [priority(50)] + + syntax HostCell + + rule [deployContract]: + deployContract(OWNER, ADDR, WASM_HASH, ARGS) + => allocObjects(ARGS) + ~> callContractFromStack(OWNER, ADDR, #quoteUnparseWasmString("init")) + ~> #resetHost + ... + + ( .Bag => + + ADDR + WASM_HASH + ... + + ) + [priority(55)] + + syntax InternalCmd ::= callContractFromStack(Address, ContractId, WasmString) [symbol(callContractFromStack)] + // ------------------------------------------------------------------------------------------------------- + rule [callContractFromStack]: + callContractFromStack(FROM, TO, FUNC) => callContract(FROM, TO, FUNC, ARGS) ... + ScVec(ARGS) : S => S + + // -------------------------------------------------------------------------------------------------------------- + rule [callTx]: + callTx(FROM, TO, FUNC, ARGS, RESULT) + => allocObjects(ARGS) + ~> callContractFromStack(FROM, TO, FUNC) + ~> expectResult(RESULT) + ~> #resetHost + ... + + // clear the host cell before contract calls + (_:HostCell => .HostStack ... ) + + syntax InternalCmd ::= expectResult(ScVal) [symbol(expectResult)] + + rule [expectResult]: + expectResult(SCVAL) => .K ... + SCVAL : .HostStack + + syntax InternalCmd ::= "#resetHost" [symbol(#resetHost)] + // -------------------------------------------------------------- + rule [resetHost]: + #resetHost => .K ... + (_:HostCell => .HostStack ... ) + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/soroban.md b/src/ksoroban/kdist/soroban-semantics/soroban.md index 43de8e7..551c80f 100644 --- a/src/ksoroban/kdist/soroban-semantics/soroban.md +++ b/src/ksoroban/kdist/soroban-semantics/soroban.md @@ -1,4 +1,182 @@ + + ```k +requires "configuration.md" +requires "switch.md" +requires "host/hostfuns.md" + +module SOROBAN-SYNTAX +endmodule + + module SOROBAN + imports SOROBAN-SYNTAX + imports CONFIG-OPERATIONS + imports SWITCH + imports HOSTFUNS +``` + +## Contract Call + +```k + + syntax InternalCmd ::= callContract ( Address, ContractId, String, List ) [symbol(callContractString), function, total] + | callContract ( Address, ContractId, WasmString, List ) [symbol(callContractWasmString)] + | callContractAux ( Address, ContractId, WasmString, List ) [symbol(callContractAux)] + // ------------------------------------------------------------------------------------- + rule callContract(FROM, TO, FUNCNAME:String, ARGS) + => callContract(FROM, TO, #quoteUnparseWasmString(FUNCNAME), ARGS) + + rule [callContract]: + callContract(FROM, TO, FUNCNAME:WasmStringToken, ARGS) + => pushWorldState + ~> pushCallState + ~> resetCallstate + ~> callContractAux(FROM, TO, FUNCNAME, ARGS) + ~> #endWasm + ... + + ... (.List => ListItem("callContract " +String #parseWasmString(FUNCNAME))) + + rule [callContractAux]: + callContractAux(FROM, TO, FUNCNAME, ARGS) + => newWasmInstance(TO, CODE) + ~> mkCall(FROM, TO, FUNCNAME, ARGS) + ... + + + TO + HASH + ... + + ... HASH |-> CODE:ModuleDecl ... + .K + + // rule [callContractAux-not-contract]: + // callContractAux(_, TO, _:WasmString, _) + // => #exception(b"not a contract: " +Bytes TO) ... + // + // + //
TO
+ // .Code + // ... + // + // .K + + syntax WasmCell + syntax InternalCmd ::= newWasmInstance (ContractId, ModuleDecl) [symbol(newWasmInstance)] + | newWasmInstanceAux(ContractId, ModuleDecl) [symbol(newWasmInstanceAux)] + + rule [newWasmInstance]: + newWasmInstance(ADDR, CODE) => newWasmInstanceAux(ADDR, CODE) ... + .K + + rule [newWasmInstanceAux]: + newWasmInstanceAux(_, CODE) => #waitWasm ~> setContractModIdx ... + ( _:WasmCell => + initContractModule(CODE) + ... + ) + // TODO: It is fairly hard to check that this rule preserves definedness. + // However, if that's not the case, then this axiom is invalid. We should + // figure this out somehow. Preferably, we should make initContractModule + // a total function. Otherwise, we should probably make a + // `definedInitContractModule` function that we should use in the requires + // clause. + + syntax InternalCmd ::= "setContractModIdx" + // ------------------------------------------------------ + rule [setContractModIdx]: + setContractModIdx => .K ... + _ => NEXTIDX -Int 1 + NEXTIDX + .K + + syntax K ::= initContractModule(ModuleDecl) [function] + // ------------------------------------------------------------------------ + rule initContractModule((module _:OptionalId _:Defns):ModuleDecl #as M) + => sequenceStmts(text2abstract(M .Stmts)) + + rule initContractModule(M:ModuleDecl) => M [owise] + + + syntax InternalCmd ::= mkCall( Address, ContractId, WasmString, List ) [symbol(mkCall)] + // ------------------------------------------------------------------------ + rule [mkCall]: + mkCall(FROM, TO, FUNCNAME:WasmStringToken, ARGS) => .K ... + + _ => FROM + _ => TO + _ => FUNCNAME + _ => ARGS + + .K => pushArgs(ARGS) ~> (invoke (FUNCADDRS {{ FUNCIDX }} orDefault -1 )) + + MODIDX + ... FUNCNAME |-> FUNCIDX:Int ... + FUNCADDRS + ... + + ... + + MODIDX:Int + ... + + requires isListIndex(FUNCIDX, FUNCADDRS) + [priority(60)] + + rule [mkCall-no-init]: + mkCall(_FROM, _TO, FUNCNAME:WasmStringToken, .List) => .K ... + + + .K + + MODIDX + EXPORTS + ... + + ... + + MODIDX:Int + ... + + requires notBool (FUNCNAME in_keys(EXPORTS)) + andBool #parseWasmString(FUNCNAME) ==K "\"init\"" + [priority(60)] + + syntax InternalInstr ::= pushArgs(List) [symbol(pushArgs)] + | pushArg(HostVal) [symbol(pushArg)] + // --------------------------------------------------------------------- + rule [pushArgs-empty]: + pushArgs(.List) => .K ... + + rule [pushArgs]: + pushArgs(ListItem(ARG:HostVal) ARGS) => pushArg(ARG) ~> pushArgs(ARGS) ... + + rule [pushArg-not-obj]: + pushArg(VAL) => VAL ... + requires notBool isObject(VAL) + + rule [pushArg-obj-rel]: + pushArg(VAL) => trap ... + requires isObject(VAL) + andBool isRelativeObjectHandle(VAL) // there should not be any relative objects in this context + + rule [pushArg-obj-abs]: + pushArg(VAL) + => fromHandleAndTag(indexToHandle(size(RELS), true) , getTag(VAL)) + ... + + RELS => RELS ListItem(VAL) + requires isObject(VAL) + andBool (notBool isRelativeObjectHandle(VAL)) + + rule [push-HostVal]: + HostVal(I) => i64.const I ... + +``` + + +```k endmodule ``` diff --git a/src/ksoroban/kdist/soroban-semantics/switch.md b/src/ksoroban/kdist/soroban-semantics/switch.md new file mode 100644 index 0000000..fb31b4d --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/switch.md @@ -0,0 +1,71 @@ +# Wasm and Host Synchronization + +The Soroban node operates with two main cells: `` for VM commands +and `` for Wasm instructions. Execution begins with ``; and when a +contract is invoked, control switches to `` for the contract's Wasm code. +If the contract execution concludes or encounters a failure, the control returns to ``. +Additionally, certain host functions, such as token transfers and contract-to-contract calls, +necessitate command execution. In these cases, control temporarily shifts to `` until +these operations are completed. +To implement synchronization between the `` and `` cells, `#endWasm`, `#waitWasm`, +and `#waitCommands` statements are utilized. + +```k +requires "configuration.md" + +module SWITCH-SYNTAX + + syntax InternalCmd ::= "#endWasm" [symbol(#endWasm)] + | "#waitWasm" [symbol(#waitWasm)] + + syntax InternalInstr ::= "#waitCommands" [symbol(#waitCommands)] + + syntax ValStack + +endmodule + +module SWITCH + imports SWITCH-SYNTAX + imports CONFIG-OPERATIONS +``` + +- `#endWasm` marks the end of the execution of Wasm instructions within a contract call. + It initiates the context switch from the current call to its parent call, and captures the Wasm + stack after the function execution. + +```k + rule [endWasm]: + #endWasm + => popCallState + ~> dropWorldState + ~> #callResult(STACK, RELS) + ... + + .K + RELS + STACK + +``` + +- `#waitWasm` is used after the `newWasmInstance` command to wait for the + completion of the Wasm module initialization. Unlike #endWasm, it doesn't manipulate the VM output + or call stack; it simply waits for the VM to finish its execution. + +```k + rule [waitWasm]: + #waitWasm => .K ... + .K +``` + +- `#waitCommands` is utilized when an instruction initiates a command. Placed in front of the `` cell, + it directs execution to continue from the `` cell until an `#endWasm` command is encountered. + +```k + rule [waitCommands]: + #waitCommands => .K ... + #endWasm ... +``` + +```k +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/ksoroban.py b/src/ksoroban/ksoroban.py new file mode 100644 index 0000000..ccc4135 --- /dev/null +++ b/src/ksoroban/ksoroban.py @@ -0,0 +1,90 @@ +from __future__ import annotations + +import sys +from argparse import ArgumentParser +from contextlib import contextmanager +from enum import Enum +from pathlib import Path +from tempfile import NamedTemporaryFile +from typing import TYPE_CHECKING + +from pyk.cli.utils import file_path +from pyk.kdist import kdist +from pyk.ktool.kprint import KAstOutput, _kast +from pyk.ktool.krun import _krun +from pykwasm.scripts.preprocessor import preprocess + +if TYPE_CHECKING: + from collections.abc import Iterator + from subprocess import CompletedProcess + + +class Backend(Enum): + LLVM = 'llvm' + HASKELL = 'haskell' + + +def main() -> None: + parser = _argument_parser() + args, rest = parser.parse_known_args() + + if args.command == 'run': + _exec_run(program=args.program, backend=args.backend) + elif args.command == 'kast': + _exec_kast(program=args.program, backend=args.backend, output=args.output) + + raise AssertionError() + + +def _exec_run(*, program: Path, backend: Backend) -> None: + definition_dir = kdist.get(f'soroban-semantics.{backend.value}') + + with _preprocessed(program) as input_file: + proc_res = _krun(definition_dir=definition_dir, input_file=input_file, check=False) + + _exit_with_output(proc_res) + + +def _exec_kast(*, program: Path, backend: Backend, output: KAstOutput | None) -> None: + definition_dir = kdist.get(f'soroban-semantics.{backend.value}') + + with _preprocessed(program) as input_file: + proc_res = _kast(input_file, definition_dir=definition_dir, output=output, check=False) + + _exit_with_output(proc_res) + + +@contextmanager +def _preprocessed(program: Path) -> Iterator[Path]: + program_text = program.read_text() + with NamedTemporaryFile() as f: + tmp_file = Path(f.name) + tmp_file.write_text(preprocess(program_text)) + yield tmp_file + + +def _exit_with_output(cp: CompletedProcess) -> None: + print(cp.stdout, end='', flush=True) + status = cp.returncode + if status: + print(cp.stderr, end='', file=sys.stderr, flush=True) + sys.exit(status) + + +def _argument_parser() -> ArgumentParser: + parser = ArgumentParser(prog='ksoroban') + command_parser = parser.add_subparsers(dest='command', required=True) + + run_parser = command_parser.add_parser('run', help='run a concrete test') + _add_common_arguments(run_parser) + + kast_parser = command_parser.add_parser('kast', help='parse a concrete test and output it in a supported format') + _add_common_arguments(kast_parser) + kast_parser.add_argument('--output', metavar='FORMAT', type=KAstOutput, help='format to output the term in') + + return parser + + +def _add_common_arguments(parser: ArgumentParser) -> None: + parser.add_argument('program', metavar='PROGRAM', type=file_path, help='path to test file') + parser.add_argument('--backend', metavar='BACKEND', type=Backend, default=Backend.LLVM, help='K backend to use') diff --git a/src/tests/integration/data/add_i32.wast b/src/tests/integration/data/add_i32.wast new file mode 100644 index 0000000..a926347 --- /dev/null +++ b/src/tests/integration/data/add_i32.wast @@ -0,0 +1,100 @@ + +setExitCode(1) + +uploadWasm( b"arith", +(module $add_i32 + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func)) + (func $add (type 0) (param i64 i64) (result i64) + (local i32 i32) + block ;; label = @1 + block ;; label = @2 + local.get 0 + i64.const 255 + i64.and + i64.const 5 + i64.ne + br_if 0 (;@2;) + local.get 1 + i64.const 255 + i64.and + i64.const 5 + i64.ne + br_if 0 (;@2;) + local.get 1 + i64.const 32 + i64.shr_u + i32.wrap_i64 + local.tee 2 + i32.const 0 + i32.lt_s + local.get 0 + i64.const 32 + i64.shr_u + i32.wrap_i64 + local.tee 3 + local.get 2 + i32.add + local.tee 2 + local.get 3 + i32.lt_s + i32.ne + br_if 1 (;@1;) + local.get 2 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 5 + i64.or + return + end + unreachable + unreachable + end + call $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE + unreachable) + (func $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE (type 1) + call $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE + unreachable) + (func $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE (type 1) + unreachable + unreachable) + (func $_ (type 1)) + (memory (;0;) 16) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048576)) + (global (;2;) i32 (i32.const 1048576)) + (export "memory" (memory 0)) + (export "add" (func $add)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2))) + +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"calculator"), + b"arith", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"calculator"), + "add", + ListItem(I32(3)) ListItem(I32(5)), + I32(8) +) + +callTx( + Account(b"test-caller"), + Contract(b"calculator"), + "add", + ListItem(I32(30000)) ListItem(I32(-50000)), + I32(-20000) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/add_u32.wast b/src/tests/integration/data/add_u32.wast new file mode 100644 index 0000000..e631a0d --- /dev/null +++ b/src/tests/integration/data/add_u32.wast @@ -0,0 +1,94 @@ + +setExitCode(1) + +uploadWasm( b"arith", + (module $add_u32 + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func)) + (func $add_u32 (type 0) (param i64 i64) (result i64) + (local i32 i32) + block ;; label = @1 + block ;; label = @2 + local.get 0 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@2;) + local.get 1 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@2;) + local.get 0 + i64.const 32 + i64.shr_u + i32.wrap_i64 + local.tee 2 + local.get 1 + i64.const 32 + i64.shr_u + i32.wrap_i64 + i32.add + local.tee 3 + local.get 2 + i32.lt_u + br_if 1 (;@1;) + local.get 3 + i64.extend_i32_u + i64.const 32 + i64.shl + i64.const 4 + i64.or + return + end + unreachable + unreachable + end + call $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE + unreachable) + (func $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE (type 1) + call $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE + unreachable) + (func $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE (type 1) + unreachable + unreachable) + (func $_ (type 1)) + (memory (;0;) 16) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048576)) + (global (;2;) i32 (i32.const 1048576)) + (export "memory" (memory 0)) + (export "add_u32" (func $add_u32)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2))) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"calculator"), + b"arith", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"calculator"), + "add_u32", + ListItem(U32(3)) ListItem(U32(5)), + U32(8) +) + +callTx( + Account(b"test-caller"), + Contract(b"calculator"), + "add_u32", + ListItem(U32(30000)) ListItem(U32(50000)), + U32(80000) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/add_u64.wast b/src/tests/integration/data/add_u64.wast new file mode 100644 index 0000000..116b3cb --- /dev/null +++ b/src/tests/integration/data/add_u64.wast @@ -0,0 +1,163 @@ + +setExitCode(1) + +uploadWasm( b"arith", +(module $add_u64 + (type (;0;) (func (param i64) (result i64))) + (type (;1;) (func (param i32 i64))) + (type (;2;) (func (param i64 i64) (result i64))) + (type (;3;) (func)) + (import "i" "0" (func $_ZN17soroban_env_guest5guest3int10obj_to_u6417hb6825d7c3a487396E (type 0))) + (import "i" "_" (func $_ZN17soroban_env_guest5guest3int12obj_from_u6417h29c7b3c8a36f37d1E (type 0))) + (func $_ZN103_$LT$u64$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17ha8dbd27463855d40E (type 1) (param i32 i64) + (local i32 i64) + block ;; label = @1 + block ;; label = @2 + local.get 1 + i32.wrap_i64 + i32.const 255 + i32.and + local.tee 2 + i32.const 64 + i32.eq + br_if 0 (;@2;) + block ;; label = @3 + local.get 2 + i32.const 6 + i32.eq + br_if 0 (;@3;) + i64.const 1 + local.set 3 + i64.const 34359740419 + local.set 1 + br 2 (;@1;) + end + local.get 1 + i64.const 8 + i64.shr_u + local.set 1 + i64.const 0 + local.set 3 + br 1 (;@1;) + end + i64.const 0 + local.set 3 + local.get 1 + call $_ZN17soroban_env_guest5guest3int10obj_to_u6417hb6825d7c3a487396E + local.set 1 + end + local.get 0 + local.get 1 + i64.store offset=8 + local.get 0 + local.get 3 + i64.store) + (func $add (type 2) (param i64 i64) (result i64) + (local i32) + global.get $__stack_pointer + i32.const 32 + i32.sub + local.tee 2 + global.set $__stack_pointer + local.get 2 + i32.const 16 + i32.add + local.get 0 + call $_ZN103_$LT$u64$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17ha8dbd27463855d40E + block ;; label = @1 + block ;; label = @2 + local.get 2 + i32.load offset=16 + br_if 0 (;@2;) + local.get 2 + i64.load offset=24 + local.set 0 + local.get 2 + local.get 1 + call $_ZN103_$LT$u64$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17ha8dbd27463855d40E + local.get 2 + i64.load + i32.wrap_i64 + br_if 0 (;@2;) + local.get 0 + local.get 2 + i64.load offset=8 + i64.add + local.tee 1 + local.get 0 + i64.lt_u + br_if 1 (;@1;) + block ;; label = @3 + block ;; label = @4 + local.get 1 + i64.const 72057594037927935 + i64.gt_u + br_if 0 (;@4;) + local.get 1 + i64.const 8 + i64.shl + i64.const 6 + i64.or + local.set 0 + br 1 (;@3;) + end + local.get 1 + call $_ZN17soroban_env_guest5guest3int12obj_from_u6417h29c7b3c8a36f37d1E + local.set 0 + end + local.get 2 + i32.const 32 + i32.add + global.set $__stack_pointer + local.get 0 + return + end + unreachable + unreachable + end + call $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE + unreachable) + (func $_ZN4core9panicking11panic_const24panic_const_add_overflow17hde776086e9d58b0fE (type 3) + call $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE + unreachable) + (func $_ZN4core9panicking9panic_fmt17h5c7ce52813e94bcdE (type 3) + unreachable + unreachable) + (func $_ (type 3)) + (memory (;0;) 16) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048576)) + (global (;2;) i32 (i32.const 1048576)) + (export "memory" (memory 0)) + (export "add" (func $add)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2))) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"calculator"), + b"arith", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"calculator"), + "add", + ListItem(U64(3)) ListItem(U64(5)), + U64(8) +) + +callTx( + Account(b"test-caller"), + Contract(b"calculator"), + "add", + ListItem(U64(1152921504606846976)) ListItem(U64(1152921504606846976)), + U64(2305843009213693952) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index dc58335..8a3fc02 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -1,5 +1,15 @@ -from ksoroban.hello import hello +from pathlib import Path +import pytest +from pyk.kdist import kdist +from pyk.ktool.krun import _krun -def test_hello() -> None: - assert hello('World') == 'Hello, World!' +TEST_DATA = (Path(__file__).parent / 'data').resolve(strict=True) +TEST_FILES = TEST_DATA.glob('*.wast') + +DEFINITION_DIR = kdist.get('soroban-semantics.llvm') + + +@pytest.mark.parametrize('program', TEST_FILES, ids=str) +def test_run(program: Path, tmp_path: Path) -> None: + _krun(input_file=program, definition_dir=DEFINITION_DIR, check=True)