diff --git a/Makefile b/Makefile index a9cdf29..20e642f 100644 --- a/Makefile +++ b/Makefile @@ -45,18 +45,12 @@ execution-test: $(EXECUTION_OUTPUTS) mx-test: $(MX_TESTING_OUTPUTS) $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) - # 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 + $$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED) $(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES) - # 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 + $$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED) $(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 53c965b..992f016 100644 --- a/mx-semantics/main/accounts/configuration.md +++ b/mx-semantics/main/accounts/configuration.md @@ -24,11 +24,4 @@ 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 b366115..bd9440e 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) - , .MxValueList + , .MxHookArgs ) => 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) - , .MxValueList + , mxStringValue(TokenId:String) + , mxIntValue(Nonce:Int) + , .MxHookArgs ) => MX#bigIntNew(mxIntValue(0)) ... Owner [priority(100)] diff --git a/mx-semantics/main/accounts/tools.md b/mx-semantics/main/accounts/tools.md deleted file mode 100644 index 80705b8..0000000 --- a/mx-semantics/main/accounts/tools.md +++ /dev/null @@ -1,152 +0,0 @@ -```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 31f7b72..22c0362 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 ( .MxValueList ) => mxIntValue(T) ... + MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ... T endmodule diff --git a/mx-semantics/main/calls/configuration.md b/mx-semantics/main/calls/configuration.md index 07d6050..c509fd8 100644 --- a/mx-semantics/main/calls/configuration.md +++ b/mx-semantics/main/calls/configuration.md @@ -1,27 +1,12 @@ ```k module MX-CALL-CONFIGURATION - imports INT-SYNTAX - imports MX-COMMON-SYNTAX - imports STRING-SYNTAX + imports STRING 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 a5ad4ef..c4076e0 100644 --- a/mx-semantics/main/calls/hooks.md +++ b/mx-semantics/main/calls/hooks.md @@ -2,40 +2,13 @@ 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 ( .MxValueList ) => mxStringValue(Caller) ... + MX#getCaller ( .MxHookArgs ) => 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 deleted file mode 100644 index ce0f98d..0000000 --- a/mx-semantics/main/communication-mocks.md +++ /dev/null @@ -1,17 +0,0 @@ -```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 17bbff2..c6f0195 100644 --- a/mx-semantics/main/configuration.md +++ b/mx-semantics/main/configuration.md @@ -7,20 +7,16 @@ 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 2d1c511..27bb479 100644 --- a/mx-semantics/main/mx-common.md +++ b/mx-semantics/main/mx-common.md @@ -1,21 +1,15 @@ ```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 559c15b..66b1315 100644 --- a/mx-semantics/main/syntax.md +++ b/mx-semantics/main/syntax.md @@ -1,67 +1,14 @@ ```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 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)] + syntax MxHookArgs ::= List{MxValue, ","} + syntax HookCall ::= MxHookName "(" MxHookArgs ")" endmodule ``` diff --git a/mx-semantics/main/tools.md b/mx-semantics/main/tools.md deleted file mode 100644 index 3e12a8d..0000000 --- a/mx-semantics/main/tools.md +++ /dev/null @@ -1,28 +0,0 @@ -```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 548d0f8..febdec7 100644 --- a/mx-semantics/targets/testing/mx.md +++ b/mx-semantics/targets/testing/mx.md @@ -2,7 +2,6 @@ requires "configuration.md" requires "../../main/mx-common.md" -requires "../../main/communication-mocks.md" requires "../../main/syntax.md" requires "../../test/execution.md" @@ -13,7 +12,6 @@ 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 0e74a35..cef680c 100644 --- a/mx-semantics/test/execution.md +++ b/mx-semantics/test/execution.md @@ -5,13 +5,11 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX imports MX-COMMON-SYNTAX imports STRING-SYNTAX - syntax TestInstruction ::= "error" - | "push" MxValue + syntax TestInstruction ::= "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) @@ -55,8 +53,8 @@ module MX-TEST-EXECUTION check_eq V => .K ... V , L:MxValueStack => L - syntax MxValueList ::= takeArgs(Int, MxValueStack) [function, total] - rule takeArgs(N:Int, _:MxValueStack) => .MxValueList + syntax MxHookArgs ::= takeArgs(Int, MxValueStack) [function, total] + rule takeArgs(N:Int, _:MxValueStack) => .MxHookArgs requires N <=Int 0 rule takeArgs(N:Int, (V:MxValue , Vs:MxValueStack)) => V , takeArgs(N -Int 1, Vs) requires 0 setCaller(S:String) => .K ... _ => S +endmodule module MX-ACCOUNTS-TEST imports private COMMON-K-CELL @@ -111,9 +110,7 @@ module MX-ACCOUNTS-TEST S .Bag - ... - [priority(100)] rule setBalance @@ -154,9 +151,6 @@ module MX-ACCOUNTS-TEST [priority(100)] - rule (.K => error) ~> setBalance(...) - [priority(200)] - endmodule module MX-BLOCKS-TEST diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md index 6dfb3ca..521da62 100644 --- a/rust-semantics/rust-common-syntax.md +++ b/rust-semantics/rust-common-syntax.md @@ -355,13 +355,13 @@ https://doc.rust-lang.org/reference/items/extern-crates.html // TypeCastExpression > left: - Expression "*" Expression [seqstrict, left] - | Expression "/" Expression [seqstrict, left] - | Expression "%" Expression [seqstrict, left] + Expression "*" Expression [strict, left] + | Expression "/" Expression [strict, left] + | Expression "%" Expression [strict, left] > left: - Expression "+" Expression [seqstrict, left] - | Expression "-" Expression [seqstrict, left] + Expression "+" Expression [strict, left] + | Expression "-" Expression [strict, left] > left: Expression "<<" Expression diff --git a/tests/execution/arithmetic-expression.1.run b/tests/execution/arithmetic-expression.1.run deleted file mode 100644 index f2e50b8..0000000 --- a/tests/execution/arithmetic-expression.1.run +++ /dev/null @@ -1,4 +0,0 @@ -new ArithmeticExpression; -call ArithmeticExpression.arithmetic_expression_mult_constant; -return_value; -check_eq 86400_u64 diff --git a/tests/execution/arithmetic-expression.2.run b/tests/execution/arithmetic-expression.2.run deleted file mode 100644 index dd0d0dc..0000000 --- a/tests/execution/arithmetic-expression.2.run +++ /dev/null @@ -1,4 +0,0 @@ -new ArithmeticExpression; -call ArithmeticExpression.arithmetic_expression_div_constant; -return_value; -check_eq 2_u64 diff --git a/tests/execution/arithmetic-expression.3.run b/tests/execution/arithmetic-expression.3.run deleted file mode 100644 index 92ab1ca..0000000 --- a/tests/execution/arithmetic-expression.3.run +++ /dev/null @@ -1,4 +0,0 @@ -new ArithmeticExpression; -call ArithmeticExpression.arithmetic_expression_sum_constant; -return_value; -check_eq 101_u64 diff --git a/tests/execution/arithmetic-expression.4.run b/tests/execution/arithmetic-expression.4.run deleted file mode 100644 index 890b7eb..0000000 --- a/tests/execution/arithmetic-expression.4.run +++ /dev/null @@ -1,4 +0,0 @@ -new ArithmeticExpression; -call ArithmeticExpression.arithmetic_expression_sub_constant; -return_value; -check_eq 99_u64 diff --git a/tests/execution/arithmetic-expression.5.run b/tests/execution/arithmetic-expression.5.run deleted file mode 100644 index f04959e..0000000 --- a/tests/execution/arithmetic-expression.5.run +++ /dev/null @@ -1,4 +0,0 @@ -new ArithmeticExpression; -call ArithmeticExpression.arithmetic_expression_mod_constant; -return_value; -check_eq 2_u64 diff --git a/tests/execution/arithmetic-expression.rs b/tests/execution/arithmetic-expression.rs deleted file mode 100644 index 6a42e70..0000000 --- a/tests/execution/arithmetic-expression.rs +++ /dev/null @@ -1,25 +0,0 @@ -#![no_std] - -#[allow(unused_imports)] -use multiversx_sc::imports::*; - -#[multiversx_sc::contract] -pub trait ArithmeticExpression { - #[init] - fn init(&self) { - } - - #[upgrade] - fn upgrade(&self) {} - - fn arithmetic_expression_mult_constant(&self) -> u64 { 24_u64 * 60_u64 * 60_u64 } - - fn arithmetic_expression_div_constant(&self) -> u64 { 10_u64 / 4_u64 } - - fn arithmetic_expression_sum_constant(&self) -> u64 { 100_u64 + 1_u64 } - - fn arithmetic_expression_sub_constant(&self) -> u64 { 100_u64 - 1_u64 } - - fn arithmetic_expression_mod_constant(&self) -> u64 { 5_u64 % 3_u64 } - -} diff --git a/tests/mx/send/send-esdt-with-function.mx b/tests/mx/send/send-esdt-with-function.mx deleted file mode 100644 index 95ca245..0000000 --- a/tests/mx/send/send-esdt-with-function.mx +++ /dev/null @@ -1,26 +0,0 @@ -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 deleted file mode 100644 index 3677d26..0000000 --- a/tests/mx/send/send-esdt.mx +++ /dev/null @@ -1,26 +0,0 @@ -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)