diff --git a/Makefile b/Makefile index 20e642f..a9cdf29 100644 --- a/Makefile +++ b/Makefile @@ -45,12 +45,18 @@ execution-test: $(EXECUTION_OUTPUTS) mx-test: $(MX_TESTING_OUTPUTS) $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) - $$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED) + # Workaround for https://github.com/runtimeverification/k/issues/4141 + -rm -r $(RUST_PREPROCESSING_KOMPILED) + $$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED) --debug $(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES) - $$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED) + # Workaround for https://github.com/runtimeverification/k/issues/4141 + -rm -r $(RUST_EXECUTION_KOMPILED) + $$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED) --debug $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) + # Workaround for https://github.com/runtimeverification/k/issues/4141 + -rm -r $(MX_TESTING_KOMPILED) $$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug $(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP) diff --git a/mx-semantics/main/accounts/configuration.md b/mx-semantics/main/accounts/configuration.md index 992f016..53c965b 100644 --- a/mx-semantics/main/accounts/configuration.md +++ b/mx-semantics/main/accounts/configuration.md @@ -24,4 +24,11 @@ module MX-ACCOUNTS-CONFIGURATION endmodule +module MX-ACCOUNTS-STACK-CONFIGURATION + imports LIST + + configuration + .List +endmodule + ``` diff --git a/mx-semantics/main/accounts/hooks.md b/mx-semantics/main/accounts/hooks.md index bd9440e..b366115 100644 --- a/mx-semantics/main/accounts/hooks.md +++ b/mx-semantics/main/accounts/hooks.md @@ -10,7 +10,7 @@ module MX-ACCOUNTS-HOOKS ( mxStringValue(Owner:String) , mxStringValue(TokenId:String) , mxIntValue(Nonce:Int) - , .MxHookArgs + , .MxValueList ) => MX#bigIntNew(mxIntValue(Balance)) ... Owner @@ -23,9 +23,9 @@ module MX-ACCOUNTS-HOOKS rule MX#bigIntGetESDTExternalBalance ( mxStringValue(Owner:String) - , mxStringValue(TokenId:String) - , mxIntValue(Nonce:Int) - , .MxHookArgs + , mxStringValue(_TokenId:String) + , mxIntValue(_Nonce:Int) + , .MxValueList ) => MX#bigIntNew(mxIntValue(0)) ... Owner [priority(100)] diff --git a/mx-semantics/main/accounts/tools.md b/mx-semantics/main/accounts/tools.md new file mode 100644 index 0000000..80705b8 --- /dev/null +++ b/mx-semantics/main/accounts/tools.md @@ -0,0 +1,152 @@ +```k + +module MX-ACCOUNTS-TOOLS + imports private BOOL + imports private COMMON-K-CELL + imports private INT + imports private MX-ACCOUNTS-CONFIGURATION + imports private MX-COMMON-SYNTAX + imports private STRING + imports private MX-ACCOUNTS-STACK-CONFIGURATION + + syntax MxInstructions ::= transferESDT + ( source: String + , destination: String + , token: String + , nonce: Int + , value: Int + ) + | checkAccountExists(address: String) + | checkESDTBalance(account: String, token: String, value: Int) + | modifyEsdtBalance(account: String, token: String, delta: Int, allowNew: Bool) + + // ------------------------------------------------------ + + rule transferESDTs(... transfers: .MxEsdtTransferList) => .K + rule (.K => transferESDT + (... source: Source, destination: Destination + , token: TokenName, nonce: Nonce, value: Value + ) + ) ~> transferESDTs + (... source: Source:String + , destination: Destination:String + , transfers: + ( mxTransferValue + (... token: TokenName:String + , nonce: Nonce:Int + , value: Value:Int + ) + , Ts:MxEsdtTransferList + ) => Ts + ) + + rule transferESDT + (... source: Source:String, destination: Destination:String + , token: TokenName:String, nonce: 0, value: Value:Int + ) + => checkAccountExists(Source) + ~> checkAccountExists(Destination) + ~> checkESDTBalance(Source, TokenName, Value) + ~> modifyEsdtBalance(Source, TokenName, 0 -Int Value, false) + ~> modifyEsdtBalance(Destination, TokenName, Value, true) + + // ------------------------------------------------------ + + rule [checkAccountExists-pass]: + checkAccountExists(Address:String) => .K ... + Address + [priority(50)] + + rule [checkAccountExists-fail]: + checkAccountExists(Address:String) + => #exception(ExecutionFailed, "account not found: " +String Address) + ... + + [priority(100)] + + + // ------------------------------------------------------ + rule [checkESDTBalance]: + checkESDTBalance(Account:String, TokenName:String, Value:Int) + => .K + ... + + Account + + TokenName + 0 + + OriginalFrom:Int + requires Value <=Int OriginalFrom + [priority(50)] + + // VALUE > ORIGFROM or TOKEN does not exist + rule [checkESDTBalance-oof-instrs-empty]: + checkESDTBalance(_, _, _) => #exception(OutOfFunds, "") ... + [priority(100)] + + // ------------------------------------------------------ + rule [modifyEsdtBalance]: + + modifyEsdtBalance + (... account: Account:String + , token: TokenName:String + , delta: Delta:Int + , allowNew: _:Bool + ) + => .K + ... + + Account + + TokenName + 0 + + OriginalFrom:Int => OriginalFrom +Int Delta + [priority(50)] + + rule [modifyEsdtBalance-new-esdtData]: + + modifyEsdtBalance + (... account: Account:String + , token: TokenName:String + , delta: Delta:Int + , allowNew: true + ) + => .K + ... + + Account + ( .Bag => + + + TokenName + 0 + + Delta + + ) + [priority(100), preserves-definedness] + + rule [modifyEsdtBalance-new-err-instrs-empty]: + modifyEsdtBalance(... account: _:String, token: _:String, delta: _:Int, allowNew: false) + => #exception(ExecutionFailed, "new ESDT data on sender") + [priority(100), preserves-definedness] + + // ------------------------------------------------------ + rule [pushWorldState]: + pushWorldState => .K ... + (.List => ListItem(ACCTDATA)) ... + ACCTDATA + rule [dropWorldState]: + dropWorldState => .K ... + (ListItem(_) => .List) ... + + // ------------------------------------------------------ + rule transferFunds(... from: From:String, to: To:String, amount: 0) + => checkAccountExists(From) + ~> checkAccountExists(To) + +endmodule + +``` diff --git a/mx-semantics/main/blocks/hooks.md b/mx-semantics/main/blocks/hooks.md index 22c0362..31f7b72 100644 --- a/mx-semantics/main/blocks/hooks.md +++ b/mx-semantics/main/blocks/hooks.md @@ -6,7 +6,7 @@ module MX-BLOCKS-HOOKS imports private MX-COMMON-SYNTAX rule - MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ... + MX#getBlockTimestamp ( .MxValueList ) => mxIntValue(T) ... T endmodule diff --git a/mx-semantics/main/calls/configuration.md b/mx-semantics/main/calls/configuration.md index c509fd8..07d6050 100644 --- a/mx-semantics/main/calls/configuration.md +++ b/mx-semantics/main/calls/configuration.md @@ -1,12 +1,27 @@ ```k module MX-CALL-CONFIGURATION - imports STRING + imports INT-SYNTAX + imports MX-COMMON-SYNTAX + imports STRING-SYNTAX configuration + "" "" + .MxValueList + 0 + .MxEsdtTransferList + 0 + 0 endmodule +module MX-CALL-RESULT-CONFIGURATION + imports MX-COMMON-SYNTAX + + configuration + .MxCallResult +endmodule + ``` \ No newline at end of file diff --git a/mx-semantics/main/calls/hooks.md b/mx-semantics/main/calls/hooks.md index c4076e0..a5ad4ef 100644 --- a/mx-semantics/main/calls/hooks.md +++ b/mx-semantics/main/calls/hooks.md @@ -2,13 +2,40 @@ module MX-CALLS-HOOKS imports private COMMON-K-CELL + imports private INT imports private MX-CALL-CONFIGURATION + imports private MX-CALL-TOOLS-SYNTAX imports private MX-COMMON-SYNTAX + imports private STRING rule - MX#getCaller ( .MxHookArgs ) => mxStringValue(Caller) ... + MX#getCaller ( .MxValueList ) => mxStringValue(Caller) ... Caller:String + rule + + MX#managedMultiTransferESDTNFTExecute + ( mxStringValue(Destination:String) + , mxTransfersValue(Transfers:MxEsdtTransferList) + , mxIntValue(_Gas:Int) + , mxStringValue("") // Function name + , mxListValue(.MxValueList) // Other arguments + ) + => (transferESDTs(Callee, Destination, Transfers) ~> mxIntValue(0)) + ... + + Callee:String + + rule + MX#managedMultiTransferESDTNFTExecute + ( mxStringValue(Destination:String) + , mxTransfersValue(Transfers:MxEsdtTransferList) + , mxIntValue(GasLimit:Int) + , mxStringValue(FunctionName:String) + , mxListValue(Args:MxValueList) + ) + => executeOnDestContext(Destination, 0, Transfers, GasLimit, FunctionName, Args) + requires 0 + Callee + Caller + Args + EgldValue + EsdtTransfers + GasLimit + 0 + + + // ----------------------------------------------------------------------------------- + rule [callContract]: + callContract + ( FunctionName:String + , + Callee + Caller + EgldValue + EsdtTransfers + _ + #as MxCallData + ) + => pushWorldState + ~> pushCallState + ~> resetCallState + ~> transferFunds(Caller, Callee, EgldValue) + ~> transferESDTs(Caller, Callee, EsdtTransfers) + ~> callContractAux + (... caller: Caller + , callee: Callee + , function: FunctionName + , input: MxCallData + ) + ~> endCall + ... + + _ => .MxCallResult + + rule [callContractAux-builtin]: + callContractAux + (... caller: From:String + , callee: To:String + , function: Function:String + , input: MxCallData:MxCallDataCell + ) + => processBuiltinFunction(toBuiltinFunction(Function), From, To, MxCallData) + requires isBuiltin(Function) + + syntax Bool ::= isBuiltin(String) [function, total] + // -------------------------------------------------------------------------- + rule isBuiltin(S:String) => toBuiltinFunction(S) =/=K #notBuiltin + + syntax BuiltinFunction ::= toBuiltinFunction(String) [function, total] + // -------------------------------------------------------------------------- + rule toBuiltinFunction(_:String) => #notBuiltin [owise] + + // -------------------------------------------------------------------------- + + syntax BuiltinFunction ::= "#ESDTTransfer" [symbol(#ESDTTransfer)] + rule toBuiltinFunction(F) => #ESDTTransfer requires F ==String "ESDTTransfer" + + rule [ESDTTransfer]: + processBuiltinFunction + ( #ESDTTransfer + , From:String + , To:String + , + EgldValue + Args + _ + #as MxCallData + ) + => checkBool(EgldValue ==Int 0, "built in function called with tx value is not allowed") + ~> checkBool(lengthValueList(Args) >=Int 2, "invalid arguments to process built-in function") + // TODO ~> check transfer to meta + // TODO ~> checkIfTransferCanHappenWithLimitedTransfer() + ~> checkBool(ESDTTransfer.value(Args) >Int 0, "negative value") + ~> transferESDTs(From, To, parseESDTTransfers(#ESDTTransfer, Args)) + ~> determineIsSCCallAfter(From, To, #ESDTTransfer, MxCallData) + + syntax String ::= "ESDTTransfer.token" "(" MxValueList ")" [function, total] + syntax Int ::= "ESDTTransfer.value" "(" MxValueList ")" [function, total] + // ----------------------------------------------------------------------------- + rule ESDTTransfer.token(ARGS) => getArgString(ARGS, 0) + rule ESDTTransfer.value(ARGS) => getArgUInt(ARGS, 1) + + syntax MxValue ::= getArg(MxValueList, Int) [function, total] + syntax String ::= getArgString(MxValueList, Int) [function, total] + syntax Int ::= getArgUInt(MxValueList, Int) [function, total] + // --------------------------------------------------------------- + rule getArg (.MxValueList, _) => mxIntValue(0) + rule getArg (_Args, I) => mxIntValue(0) requires I A + rule getArg ((_A , Args), I) => getArg(Args, I -Int 1) requires I >Int 0 + rule getArgString(Args, I) => getMxString(getArg(Args, I)) + rule getArgUInt (ARGS, I) => getMxUint(getArg(ARGS, I)) + + syntax MxInstructions ::= determineIsSCCallAfter(String, String, BuiltinFunction, MxCallDataCell) + [symbol(determineIsSCCallAfter)] + // ---------------------------------------------- + rule [determineIsSCCallAfter-nocall]: + determineIsSCCallAfter + (_SND, _DST, FUNC + , + Args:MxValueList + ... + + ) + => .K + requires getCallFunc(FUNC, Args) ==K "" + + syntax String ::= getCallFunc(BuiltinFunction, MxValueList) [function, total] + // -------------------------------------------------------------------------- + rule getCallFunc(#ESDTTransfer, ARGS) => getArgString(ARGS, 2) // token&amount&func&... + // rule getCallFunc(#ESDTNFTTransfer, ARGS) => getArgString(ARGS, 4) // token&nonce&amount&dest&func&... + // rule getCallFunc(#MultiESDTNFTTransfer, ARGS) + // => getArg(ARGS, MultiESDTNFTTransfer.num(ARGS) *Int 3 +Int 2) + rule getCallFunc(_, _) => "" [owise] + + syntax MxEsdtTransferList ::= parseESDTTransfers(BuiltinFunction, MxValueList) [function, total] + // ------------------------------------------------------------------------------------ + rule parseESDTTransfers(#ESDTTransfer, ARGS) + => mxTransferValue(... token: ESDTTransfer.token(ARGS), nonce: 0, value: ESDTTransfer.value(ARGS)), + .MxEsdtTransferList + + rule parseESDTTransfers(_, _) => .MxEsdtTransferList + [owise] + + // ------------------------------------------------------ + rule [executeOnDestContext]: + executeOnDestContext + (... destination: Destination:String + , egldValue: Value:Int + , esdtTransfers: Esdt:MxEsdtTransferList + , gasLimit: GasLimit:Int + , function: Func:String + , args: Args:MxValueList + ) + => callContract + ( Func + , prepareIndirectContractCallInput + (... caller: Callee + , callee: Destination + , egldValue: Value + , esdtTransfers: Esdt + , gasLimit: GasLimit + , args:Args + ) + ) + ~> finishExecuteOnDestContext + ... + + Callee + + // ------------------------------------------------------ + rule [finishExecuteOnDestContext-ok]: + finishExecuteOnDestContext => mxIntValue(0) ... + mxCallResult(... returnCode: OK) => .MxCallResult + + rule [finishExecuteOnDestContext-exception]: + finishExecuteOnDestContext => resolveErrorFromOutput(EC, MSG) ... + mxCallResult(... returnCode: EC:ExceptionCode, returnMessage: MSG) => .MxCallResult + + // TODO: This does not always return correct codes/messages. The messages + // below are optimized for debugability. + syntax MxInstructions ::= resolveErrorFromOutput(ExceptionCode, String) [function, total] + // ----------------------------------------------------------------------- + rule resolveErrorFromOutput(ExecutionFailed, Msg:String) + => #exception(ExecutionFailed, Msg) + rule resolveErrorFromOutput(FunctionNotFound, Msg) + => #exception(ExecutionFailed, "Function not found: " +String Msg) + rule resolveErrorFromOutput(UserError, Msg) + => #exception + ( ExecutionFailed + , #if Msg ==K "action is not allowed" + #then Msg + #else "error signalled by smartcontract: " +String Msg + #fi + ) + rule resolveErrorFromOutput(OutOfFunds, Msg) + => #exception(ExecutionFailed, "failed transfer (insufficient funds): " +String Msg) + rule resolveErrorFromOutput(EC, Msg) + => #exception(EC, Msg) + [owise] + + // ----------------------------------------------------------------------- + rule [endCall]: + endCall + => asyncExecute + ~> setVMOutput + ~> popCallState + ~> dropWorldState + + rule [setVMOutput]: + setVMOutput => .K ... + + _ => mxCallResult + (... returnCode: OK + , returnMessage: "" + , out: mxUnitValue() + ) + + + // TODO: Not implemented. + rule asyncExecute => .K + +endmodule + +``` \ No newline at end of file diff --git a/mx-semantics/main/communication-mocks.md b/mx-semantics/main/communication-mocks.md new file mode 100644 index 0000000..ce0f98d --- /dev/null +++ b/mx-semantics/main/communication-mocks.md @@ -0,0 +1,17 @@ +```k + +module MX-COMMUNICATION-MOCKS + imports MX-COMMON-SYNTAX + + // TODO: These should save/restore the `` cell. It should be implemented in + // the part of the semantics that binds mx with rust. + rule pushCallState => .K + rule popCallState => .K + + // TODO: This should reset the rust cell. It should be implemented in + // the part of the semantics that binds mx with rust. + rule resetCallState => .K + +endmodule + +``` diff --git a/mx-semantics/main/configuration.md b/mx-semantics/main/configuration.md index c6f0195..17bbff2 100644 --- a/mx-semantics/main/configuration.md +++ b/mx-semantics/main/configuration.md @@ -7,16 +7,20 @@ requires "calls/configuration.md" module MX-COMMON-CONFIGURATION imports MX-ACCOUNTS-CONFIGURATION + imports MX-ACCOUNTS-STACK-CONFIGURATION imports MX-BIGUINT-CONFIGURATION imports MX-BLOCKS-CONFIGURATION imports MX-CALL-CONFIGURATION + imports MX-CALL-RESULT-CONFIGURATION configuration + + endmodule diff --git a/mx-semantics/main/mx-common.md b/mx-semantics/main/mx-common.md index 27bb479..2d1c511 100644 --- a/mx-semantics/main/mx-common.md +++ b/mx-semantics/main/mx-common.md @@ -1,15 +1,21 @@ ```k requires "accounts/hooks.md" +requires "accounts/tools.md" requires "biguint/hooks.md" requires "blocks/hooks.md" requires "calls/hooks.md" +requires "calls/tools.md" +requires "tools.md" module MX-COMMON imports private MX-ACCOUNTS-HOOKS + imports private MX-ACCOUNTS-TOOLS imports private MX-BIGUINT-HOOKS imports private MX-BLOCKS-HOOKS imports private MX-CALLS-HOOKS + imports private MX-CALLS-TOOLS + imports private MX-TOOLS endmodule ``` \ No newline at end of file diff --git a/mx-semantics/main/syntax.md b/mx-semantics/main/syntax.md index 66b1315..559c15b 100644 --- a/mx-semantics/main/syntax.md +++ b/mx-semantics/main/syntax.md @@ -1,14 +1,67 @@ ```k module MX-COMMON-SYNTAX + imports BOOL-SYNTAX imports INT-SYNTAX imports STRING-SYNTAX + syntax MxEsdtTransfer ::= mxTransferValue(token:String, nonce:Int, value:Int) + syntax MxEsdtTransferList ::= List{MxEsdtTransfer, ","} + syntax MxValue ::= mxIntValue(Int) | mxStringValue(String) + | mxListValue(MxValueList) + | MxEsdtTransfer + | mxTransfersValue(MxEsdtTransferList) + | mxUnitValue() syntax MxHookName ::= r"MX#[a-zA-Z][a-zA-Z0-9]*" [token] - syntax MxHookArgs ::= List{MxValue, ","} - syntax HookCall ::= MxHookName "(" MxHookArgs ")" + syntax MxValueList ::= List{MxValue, ","} + syntax HookCall ::= MxHookName "(" MxValueList ")" + + syntax Int ::= lengthValueList(MxValueList) [function, total] + syntax String ::= getMxString(MxValue) [function, total] + syntax Int ::= getMxUint(MxValue) [function, total] + + syntax BuiltinFunction ::= "#notBuiltin" [symbol(#notBuiltin)] + syntax MxCallDataCell + + syntax MxInstructions ::= transferESDTs + ( source: String + , destination: String + , transfers: MxEsdtTransferList + ) + | transferFunds(from: String, to: String, amount: Int) + | #exception(ExceptionCode, String) + | "pushCallState" [symbol(pushCallState)] + | "popCallState" [symbol(popCallState)] + | "resetCallState" [symbol(resetCallState)] + | "pushWorldState" [symbol(pushWorldState)] + | "dropWorldState" [symbol(dropWorldState)] + | processBuiltinFunction(BuiltinFunction, String, String, MxCallDataCell) + [symbol(processBuiltinFunction)] + | checkBool(Bool, String) [symbol(checkBool)] + + syntax MxCallResult ::= ".MxCallResult" + | mxCallResult + ( returnCode: ReturnCode + , returnMessage: String + , out: MxValue + ) [symbol(mxCallResult)] + + syntax ReturnCode ::= "OK" [symbol(OK)] + | ExceptionCode + syntax ExceptionCode ::= "FunctionNotFound" [symbol(FunctionNotFound)] + | "FunctionWrongSignature" [symbol(FunctionWrongSignature)] + | "ContractNotFound" [symbol(ContractNotFound)] + | "UserError" [symbol(UserError)] + | "OutOfGas" [symbol(OutOfGas)] + | "AccountCollision" [symbol(AccountCollision)] + | "OutOfFunds" [symbol(OutOfFunds)] + | "CallStackOverFlow" [symbol(CallStackOverFlow)] + | "ContractInvalid" [symbol(ContractInvalid)] + | "ExecutionFailed" [symbol(ExecutionFailed)] + | "UpgradeFailed" [symbol(UpgradeFailed)] + | "SimulateFailed" [symbol(SimulateFailed)] endmodule ``` diff --git a/mx-semantics/main/tools.md b/mx-semantics/main/tools.md new file mode 100644 index 0000000..3e12a8d --- /dev/null +++ b/mx-semantics/main/tools.md @@ -0,0 +1,28 @@ +```k + +module MX-TOOLS + imports private BOOL + imports private INT + imports private MX-COMMON-SYNTAX + + // --------------------------------------------------------------- + rule getMxString(mxStringValue(S)) => S + rule getMxString(_) => "" [owise] + rule getMxUint(mxIntValue(V)) => V requires V >=Int 0 + rule getMxUint(_) => 0 [owise] + + // ----------------------------------------------------------------------------- + rule [checkBool-t]: + checkBool(B, _) => .K requires B + rule [checkBool-f]: + checkBool(B, ERR) => #exception(ExecutionFailed, ERR) requires notBool B + + // ----------------------------------------------------------------------------- + rule lengthValueList(.MxValueList) => 0 + rule lengthValueList(_ , L:MxValueList) => 1 +Int lengthValueList(L) + // Fix for https://github.com/runtimeverification/k/issues/4587 + rule lengthValueList(_) => 0 [owise] + +endmodule + +``` \ No newline at end of file diff --git a/mx-semantics/targets/testing/mx.md b/mx-semantics/targets/testing/mx.md index febdec7..548d0f8 100644 --- a/mx-semantics/targets/testing/mx.md +++ b/mx-semantics/targets/testing/mx.md @@ -2,6 +2,7 @@ requires "configuration.md" requires "../../main/mx-common.md" +requires "../../main/communication-mocks.md" requires "../../main/syntax.md" requires "../../test/execution.md" @@ -12,6 +13,7 @@ endmodule module MX imports private MX-COMMON + imports private MX-COMMUNICATION-MOCKS imports private MX-CONFIGURATION imports private MX-TEST-EXECUTION endmodule diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md index cef680c..4c19bad 100644 --- a/mx-semantics/test/execution.md +++ b/mx-semantics/test/execution.md @@ -5,11 +5,13 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX imports MX-COMMON-SYNTAX imports STRING-SYNTAX - syntax TestInstruction ::= "push" MxValue + syntax TestInstruction ::= "error" + | "push" MxValue | "call" argcount:Int MxHookName | "get_big_int" | getBigint(Int) | "check_eq" MxValue + | setCallee(String) | setCaller(String) | addAccount(String) | setBalance(account:String, token:String, nonce:Int, value:Int) @@ -53,8 +55,8 @@ module MX-TEST-EXECUTION check_eq V => .K ... V , L:MxValueStack => L - syntax MxHookArgs ::= takeArgs(Int, MxValueStack) [function, total] - rule takeArgs(N:Int, _:MxValueStack) => .MxHookArgs + syntax MxValueList ::= takeArgs(Int, MxValueStack) [function, total] + rule takeArgs(N:Int, _:MxValueStack) => .MxValueList requires N <=Int 0 rule takeArgs(N:Int, (V:MxValue , Vs:MxValueStack)) => V , takeArgs(N -Int 1, Vs) requires 0 setCallee(S:String) => .K ... + _ => S + rule setCaller(S:String) => .K ... _ => S @@ -102,6 +108,10 @@ module MX-ACCOUNTS-TEST imports private MX-ACCOUNTS-CONFIGURATION imports private MX-TEST-EXECUTION-PARSING-SYNTAX + rule + (.K => error) ~> addAccount(S:String) ... + S + [priority(50)] rule addAccount(S:String) => .K ... @@ -110,7 +120,9 @@ module MX-ACCOUNTS-TEST S .Bag + ... + [priority(100)] rule setBalance @@ -151,6 +163,9 @@ module MX-ACCOUNTS-TEST [priority(100)] + rule (.K => error) ~> setBalance(...) + [priority(200)] + endmodule module MX-BLOCKS-TEST diff --git a/tests/mx/send/send-esdt-with-function.mx b/tests/mx/send/send-esdt-with-function.mx new file mode 100644 index 0000000..95ca245 --- /dev/null +++ b/tests/mx/send/send-esdt-with-function.mx @@ -0,0 +1,26 @@ +addAccount("Sender"); +addAccount("Receiver"); +setBalance("Sender", "MyToken", 0, 1234); +setCallee("Sender"); + +push mxListValue(mxStringValue("MyToken"), mxIntValue(100)); +push mxStringValue("ESDTTransfer"); +push mxIntValue(0); +push mxTransfersValue(); +push mxStringValue("Receiver"); +call 5 MX#managedMultiTransferESDTNFTExecute; +check_eq mxIntValue(0); + +push mxIntValue(0); +push mxStringValue("MyToken"); +push mxStringValue("Sender"); +call 3 MX#bigIntGetESDTExternalBalance; +get_big_int; +check_eq mxIntValue(1134); + +push mxIntValue(0); +push mxStringValue("MyToken"); +push mxStringValue("Receiver"); +call 3 MX#bigIntGetESDTExternalBalance; +get_big_int; +check_eq mxIntValue(100) diff --git a/tests/mx/send/send-esdt.mx b/tests/mx/send/send-esdt.mx new file mode 100644 index 0000000..3677d26 --- /dev/null +++ b/tests/mx/send/send-esdt.mx @@ -0,0 +1,26 @@ +addAccount("Sender"); +addAccount("Receiver"); +setBalance("Sender", "MyToken", 0, 1234); +setCallee("Sender"); + +push mxListValue(); +push mxStringValue(""); +push mxIntValue(0); +push mxTransfersValue(mxTransferValue("MyToken", 0, 100)); +push mxStringValue("Receiver"); +call 5 MX#managedMultiTransferESDTNFTExecute; +check_eq mxIntValue(0); + +push mxIntValue(0); +push mxStringValue("MyToken"); +push mxStringValue("Sender"); +call 3 MX#bigIntGetESDTExternalBalance; +get_big_int; +check_eq mxIntValue(1134); + +push mxIntValue(0); +push mxStringValue("MyToken"); +push mxStringValue("Receiver"); +call 3 MX#bigIntGetESDTExternalBalance; +get_big_int; +check_eq mxIntValue(100)