diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index d0468764..14b12b57 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmultiversx" -version = "0.1.57" +version = "0.1.58" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md index 1d627699..a0dde739 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md @@ -463,6 +463,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
ADDR
... + (#waitCommands ~> _) #Or .K // S => S +String " -- initAccount duplicate " +String Bytes2String(ADDR) [priority(60)] @@ -477,6 +478,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond ) ... + (#waitCommands ~> _) #Or .K // S => S +String " -- initAccount new " +String Bytes2String(ADDR) [priority(61)] @@ -495,6 +497,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond _ => STORAGE ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [setAccountCode]: @@ -504,6 +507,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond _ => CODE ... + (#waitCommands ~> _) #Or .K [priority(60)] rule setAccountOwner(ADDR, OWNER) => .K ... @@ -512,6 +516,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond _ => OWNER ... + (#waitCommands ~> _) #Or .K [priority(60)] ``` @@ -532,6 +537,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond ~> transferFundsH(A, B, V) ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [transferFundsH-self]: @@ -544,6 +550,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond ORIGFROM ... + (#waitCommands ~> _) #Or .K requires VALUE <=Int ORIGFROM [priority(60)] @@ -562,6 +569,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond ORIGTO => ORIGTO +Int VALUE ... + (#waitCommands ~> _) #Or .K requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM [priority(60), preserves-definedness] // Preserving definedness: @@ -575,6 +583,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond ORIGFROM ... + (#waitCommands ~> _) #Or .K requires VALUE >Int ORIGFROM [priority(60)] @@ -589,6 +598,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond rule callContract(TO, FUNCNAME:String, VMINPUT) => callContract(TO, #quoteUnparseWasmString(FUNCNAME), VMINPUT) ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [callContract]: @@ -617,6 +627,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond _ => .VMOutput S => S +String " -- callContract " +String #parseWasmString(FUNCNAME) + (#waitCommands ~> _) #Or .K requires notBool(isBuiltin(FUNCNAME)) andBool #token("\"callBack\"", "WasmStringToken") =/=K FUNCNAME [priority(60)] @@ -640,6 +651,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond _ => .VMOutput S => S +String " -- callContract " +String #parseWasmString(FUNC) + (#waitCommands ~> _) #Or .K requires isBuiltin(FUNC) [priority(60)] @@ -647,6 +659,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond callContract(_, FUNCNAME:WasmString, _) => #throwExceptionBs(ExecutionFailed, b"invalid function (calling callBack() directly is forbidden)") ... + (#waitCommands ~> _) #Or .K requires #token("\"callBack\"", "WasmStringToken") ==K FUNCNAME [priority(60)] @@ -659,12 +672,14 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond .Code ... + (#waitCommands ~> _) #Or .K [priority(61)] rule [callContract-not-found]: callContract(TO, _:WasmString, _) => #throwExceptionBs(ExecutionFailed, b"account not found: " +Bytes TO) ... + (#waitCommands ~> _) #Or .K [priority(62)] ``` @@ -675,6 +690,7 @@ Every contract call runs in its own Wasm instance initialized with the contract' // -------------------------------------------------------------------------------------------------- rule [newWasmInstance]: newWasmInstance(ADDR, CODE) => newWasmInstanceAux(ADDR, CODE) ... + .K rule [newWasmInstanceAux]: newWasmInstanceAux(_, CODE) => #waitWasm ~> setContractModIdx ... diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md index 261a400f..e7ce5424 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md @@ -5,9 +5,11 @@ TODO check token settings: frozen, paused, limited transfer... ```k requires "elrond-node.md" +requires "switch.md" module ESDT imports ELROND-NODE + imports SWITCH-SYNTAX imports LIST-BYTES-EXTENSIONS imports MAP-BYTES-TO-BYTES-PRIMITIVE @@ -29,13 +31,17 @@ module ESDT ~> appendToOutAccount(TO, OutputTransfer(FROM, L)) ... + (#waitCommands ~> _) #Or .K rule transferESDTsAux(_, _, .List) => .K ... + (#waitCommands ~> _) #Or .K + rule transferESDTsAux(FROM, TO, ListItem(T:ESDTTransfer) Ls) => transferESDT(FROM, TO, T) ~> transferESDTsAux(FROM, TO, Ls) ... + (#waitCommands ~> _) #Or .K rule transferESDT(FROM, TO, esdtTransfer(TOKEN, VALUE, 0)) => checkAccountExists(FROM) @@ -45,6 +51,7 @@ module ESDT ~> addToESDTBalance(TO, TOKEN, VALUE, true) ... + (#waitCommands ~> _) #Or .K rule transferESDT(FROM, TO, esdtTransfer(TOKEN, VALUE, NONCE)) => checkAccountExists(FROM) @@ -54,6 +61,7 @@ module ESDT ~> removeEmptyNft(FROM, keyWithNonce(TOKEN, NONCE)) ... + (#waitCommands ~> _) #Or .K requires NONCE =/=Int 0 syntax InternalCmd ::= removeEmptyNft(Bytes, Bytes) @@ -69,10 +77,12 @@ module ESDT => .Bag) ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [removeEmptyNft-skip]: removeEmptyNft(_, _) => .K ... + (#waitCommands ~> _) #Or .K [priority(61)] ``` @@ -95,12 +105,14 @@ module ESDT ... + (#waitCommands ~> _) #Or .K requires VALUE <=Int ORIGFROM [priority(60)] // VALUE > ORIGFROM or TOKEN does not exist rule [checkESDTBalance-oof]: checkESDTBalance(_, _, _) => #throwExceptionBs(OutOfFunds, b"") ... + (#waitCommands ~> _) #Or .K [priority(61)] ``` @@ -121,6 +133,7 @@ module ESDT ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [addToESDTBalance-new-esdtData]: @@ -134,6 +147,7 @@ module ESDT ) ... + (#waitCommands ~> _) #Or .K [priority(61)] rule [addToESDTBalance-new-err]: @@ -141,6 +155,7 @@ module ESDT => #throwExceptionBs(ExecutionFailed, b"new NFT data on sender") ... + (#waitCommands ~> _) #Or .K [priority(61)] ``` @@ -170,6 +185,7 @@ module ESDT ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [moveNFTToDestination-self]: @@ -182,6 +198,7 @@ module ESDT ... + (#waitCommands ~> _) #Or .K [priority(60)] rule [moveNFTToDestination-new]: @@ -206,6 +223,7 @@ module ESDT ) ... + (#waitCommands ~> _) #Or .K [priority(61)] ``` @@ -233,20 +251,11 @@ module ESDT ~> checkAllowedToExecute(SND, getArg(ARGS, 0), ESDTRoleLocalMint) ~> checkBool( lengthBytes(getArg(ARGS, 1)) <=Int 100 , "invalid arguments to process built-in function") - ~> esdtLocalMint( SND - , getArg(ARGS, 0) - , getArgUInt(ARGS, 1) - ) + ~> addToESDTBalance(SND, getArg(ARGS, 0), getArgUInt(ARGS, 1), true) ... + .K - syntax InternalCmd ::= esdtLocalMint(account: Bytes, token: Bytes, value: Int) - [symbol(esdtLocalMint)] - // ------------------------------------------------------------------------------ - rule [esdtLocalMint-cmd]: - esdtLocalMint(ADDR, TOK, VAL) - => addToESDTBalance(ADDR, TOK, VAL, true) ... - ``` ### Local Burn @@ -272,22 +281,11 @@ module ESDT ~> checkAllowedToExecute(SND, getArg(ARGS, 0), ESDTRoleLocalBurn) ~> checkBool( lengthBytes(getArg(ARGS, 1)) <=Int 100 , "invalid arguments to process built-in function") - ~> esdtLocalBurn( SND - , getArg(ARGS, 0) - , getArgUInt(ARGS, 1) - ) - ... - - - syntax InternalCmd ::= esdtLocalBurn(account: Bytes, token: Bytes, value: Int) - [symbol(esdtLocalBurn)] - // ------------------------------------------------------------------------------ - rule [esdtLocalBurn-cmd]: - esdtLocalBurn(ADDR, TOK, VAL) - => checkESDTBalance(ADDR, TOK, VAL) - ~> addToESDTBalance(ADDR, TOK, 0 -Int VAL, false) + ~> checkESDTBalance(SND, getArg(ARGS, 0), getArgUInt(ARGS, 1)) + ~> addToESDTBalance(SND, getArg(ARGS, 0), 0 -Int getArgUInt(ARGS, 1), false) ... + .K ``` @@ -317,6 +315,7 @@ module ESDT ) ... + .K syntax InternalCmd ::= esdtNftBurn(Bytes, Bytes, Int, Int) // ---------------------------------------------------------- @@ -328,6 +327,7 @@ module ESDT ~> removeEmptyNft(ADDR, keyWithNonce(TOKEN, NONCE)) ... + .K ``` @@ -356,6 +356,7 @@ module ESDT ~> determineIsSCCallAfter(SND, DST, #ESDTTransfer, VMINPUT) ... + .K syntax Bytes ::= "ESDTTransfer.token" "(" ListBytes ")" [function, total] syntax Int ::= "ESDTTransfer.value" "(" ListBytes ")" [function, total] @@ -386,12 +387,14 @@ module ESDT CODE:ModuleDecl ... + .K requires getCallFunc(FUNC, ARGS) =/=K b"" rule [determineIsSCCallAfter-nocall]: determineIsSCCallAfter(_SND, _DST, _FUNC, _VMINPUT) => .K ... + .K [owise] syntax VmInputCell ::= mkVmInputEsdtExec(Bytes, BuiltinFunction, ListBytes, Int, Int, Bytes) @@ -443,6 +446,7 @@ module ESDT ~> determineIsSCCallAfter(SND, MultiESDTNFTTransfer.dest(ARGS), #MultiESDTNFTTransfer, VMINPUT) ... + .K syntax Bytes ::= "MultiESDTNFTTransfer.dest" "(" ListBytes ")" [function, total] @@ -506,6 +510,7 @@ module ESDT ~> esdtNftCreate(SND, ESDTNFTCreate.token(ARGS), ESDTNFTCreate.qtty(ARGS), ESDTNFTCreate.meta(SND, ARGS)) ... + .K syntax InternalCmd ::= esdtNftCreate(Bytes, Bytes, Int, ESDTMetadata) [symbol(esdtNftCreate)] // --------------------------------------------------------------------------------------------------------- @@ -524,6 +529,7 @@ module ESDT ~> saveLatestNonce(SND, TOKEN, NONCE) ... + .K syntax Bytes ::= "ESDTNFTCreate.token" "(" ListBytes ")" [function, total] syntax Int ::= "ESDTNFTCreate.qtty" "(" ListBytes ")" [function, total] @@ -576,6 +582,7 @@ module ESDT ... ... (.ListBytes => ListItem(wrap(Int2Bytes(NONCE, BE, Unsigned)))) + .K syntax InternalCmd ::= saveLatestNonce(Bytes, Bytes, Int) [symbol(saveLatestNonce)] // --------------------------------------------------------------------------------------------- @@ -590,6 +597,7 @@ module ESDT ... + .K ``` ### NFT Add Quantity @@ -622,6 +630,7 @@ module ESDT ) ... + .K syntax InternalCmd ::= esdtNftAddQuantity(Bytes, Bytes, Int, Int) // ----------------------------------------------------------------- @@ -637,6 +646,7 @@ module ESDT ) ... + .K ``` @@ -665,6 +675,7 @@ module ESDT ~> determineIsSCCallAfter(SND, getArg(ARGS, 3), #ESDTNFTTransfer, VMINPUT) ... + .K ``` @@ -697,6 +708,7 @@ module ESDT ) ... + .K [priority(60)] syntax InternalCmd ::= esdtNftAddUri(Bytes, Bytes, ListBytes) @@ -714,12 +726,14 @@ module ESDT ... + .K [priority(60)] rule [esdtNftAddUri-not-found]: esdtNftAddUri(_SND, _TOKEN, _NEW_URIS) => #throwExceptionBs(UserError, b"new NFT data on sender") ... + .K [priority(61)] ``` @@ -742,6 +756,7 @@ module ESDT // ---------------------------------------------------------------------------------------- rule [checkAllowedToExecute-system]: checkAllowedToExecute(#esdtSCAddress, _, _) => .K ... + .K rule [checkAllowedToExecute-pass]: checkAllowedToExecute(ADDR, TOK, ROLE) => .K ... @@ -754,6 +769,7 @@ module ESDT ... + .K requires ROLE in ROLES [priority(60)] @@ -761,6 +777,7 @@ module ESDT checkAllowedToExecute(_ADDR, _TOK, _ROLE) => #throwExceptionBs(UserError, b"action is not allowed") ... + .K [priority(61)] syntax ListBytes ::= getCallArgs(BuiltinFunction, ListBytes) [function, total] diff --git a/package/version b/package/version index 920c3bd5..61671068 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.57 +0.1.58