Implement call_value()

mx-rust-semantics/main/expression/mx-to-rust.md

@@ -4,13 +4,17 @@ module MX-RUST-EXPRESSION-MX-TO-RUST
     imports private K-EQUAL-SYNTAX
     imports private MX-COMMON-SYNTAX
     imports private MX-RUST-REPRESENTATION
+    imports private RUST-ERROR-SYNTAX
     imports private RUST-HELPERS
     imports private RUST-VALUE-SYNTAX
 
     syntax Bool ::= isMxToRustValue(K)  [function, total, symbol(isMxToRustValue)]
     rule isMxToRustValue(_:K) => false [owise]
     rule isMxToRustValue(_:PtrValue) => true
     rule isMxToRustValue(mxToRustField(_, V:MxToRust)) => isMxToRustValue(V)
+    rule isMxToRustValue(.MxToRustList) => true
+    rule isMxToRustValue(V:MxToRust , Vs:MxToRustList)
+        => isMxToRustValue(V) andBool isMxToRustValue(Vs)
 
     syntax Bool ::= isMxToRustFieldValue(K)  [function, total, symbol(isMxToRustFieldValue)]
     rule isMxToRustFieldValue(_:K) => false [owise]
@@ -32,6 +36,11 @@ module MX-RUST-EXPRESSION-MX-TO-RUST
             , mxListValue(Values:MxValueList)
             )
         => mxToRustStruct(StructName, pairFields(Fields, Values))
+    rule mxToRustTyped
+            ( (Types:NonEmptyTypeCsv)
+            , mxListValue(Values:MxValueList)
+            )
+        => mxToRustTuple(pairTuple(Types, Values))
     rule mxToRustTyped(() , mxUnitValue()) => ptrValue(null, tuple(.ValueList))
 
     context HOLE:MxRustFieldValue , _:MxRustFieldValues [result(MxToRustFieldValue)]
@@ -80,6 +89,40 @@ module MX-RUST-EXPRESSION-MX-TO-RUST
     rule fieldsToMap((Field , _:MxRustFieldValues), _:Map)
         => error("Unexpected field", ListItem(Field))
         [owise]
+
+    rule (.K => mxToRustListToValueList(L)) ~> mxToRustTuple(L:MxToRustList)
+        requires isMxToRustValue(L)
+    rule (L:ValueList ~> mxToRustTuple(_:MxToRustList))
+        => mxRustNewValue(tuple(L))
+
+    syntax ValueListOrError ::= mxToRustListToValueList(MxToRustList)  [function, total]
+    rule mxToRustListToValueList(.MxToRustList) => .ValueList
+    rule mxToRustListToValueList(ptrValue(_, V:Value) , L:MxToRustList)
+        => concat(V, mxToRustListToValueList(L))
+    rule mxToRustListToValueList(L) => error("mxToRustListToValueList: not evaluated", ListItem(L))
+        [owise]
+
+    context HOLE:MxToRust , _:MxToRustList [result(MxToRustValue)]
+    context V:MxToRust , HOLE:MxToRustList requires isMxToRustValue(V)
+        [result(MxToRustValue)]
+
+    syntax MxToRustList ::= pairTuple(NonEmptyTypeCsv, MxValueList)  [function, total]
+    rule pairTuple(T:Type, V:MxValue , .MxValueList)
+        => mxToRustTyped(T, V) , .MxToRustList
+    rule pairTuple
+            ( T:Type , Ts:NonEmptyTypeCsv
+            , V:MxValue , Vs:MxValueList
+            )
+        => mxToRustTyped(T, V) , pairTuple(Ts, Vs)
+
+    rule pairTuple(Ts:NonEmptyTypeCsv, .MxValueList)
+        => error("Not enough values (pairTuple)", ListItem(Ts))
+    rule pairTuple(T:Type, (_ , _ , _:MxValueList) #as L)
+        => error("Not enough types (pairTuple)", ListItem(T) ListItem(L))
+    rule pairTuple(A, B)
+        => error("Should not happen (pairTuple)", ListItem(A) ListItem(B))
+        [owise]
+
 endmodule
 
 ```

mx-rust-semantics/main/expression/rust-to-mx.md

@@ -24,6 +24,9 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
         </k>
         <values> Values:Map </values>
         [owise]
+    rule rustToMx(tuple(V:ValueList))
+        => rustValuesToMxListValue(V, .MxValueList)
+    rule rustToMx(B:Bool => mxBoolValue(B))
     rule rustToMx(S:String => mxStringValue(S))
     rule rustToMx(V:Value => mxIntValue({valueToInteger(V)}:>Int))
         requires notBool isSemanticsError(valueToInteger(V))

mx-rust-semantics/main/glue.md

@@ -58,12 +58,9 @@ module MX-RUST-GLUE
 
     rule ptrValue(_, V) ~> rustValueToMx => rustValueToMx(V)
 
-    rule rustValueToMx(tuple(.ValueList)) => mxUnitValue()
-    rule rustValueToMx(B:Bool) => mxBoolValue(B)
-    rule rustValueToMx(S:String) => mxStringValue(S)
-    
-    rule rustValueToMx(V:Value) => mxIntValue({valueToInteger(V)}:>Int)
-        requires notBool isSemanticsError(valueToInteger(V))
+    rule (.K => rustToMx(V)) ~> rustValueToMx(V:Value)
+        [owise]
+    rule (rustToMx(V:MxValue) ~> rustValueToMx(_)) => V
 
     rule mxIntValue(0) ~> mxRustCheckMxStatus => .K
 

mx-rust-semantics/main/modules.md

@@ -2,6 +2,7 @@
 
 requires "modules/address.md"
 requires "modules/biguint.md"
+requires "modules/call-value.md"
 requires "modules/hooks.md"
 requires "modules/proxy.md"
 requires "modules/send.md"
@@ -11,6 +12,7 @@ requires "modules/token-identifier.md"
 module MX-RUST-MODULES
     imports private MX-RUST-MODULES-ADDRESS
     imports private MX-RUST-MODULES-BIGUINT
+    imports private MX-RUST-MODULES-CALL-VALUE
     imports private MX-RUST-MODULES-HOOKS
     imports private MX-RUST-MODULES-PROXY
     imports private MX-RUST-MODULES-SEND

mx-rust-semantics/main/modules/biguint.md

@@ -26,7 +26,6 @@ module MX-RUST-MODULES-BIGUINT
         <values> ValueId |-> V:Value ... </values>
 
   // --------------------------------------
-    syntax MxRustType ::= "bigUintType"  [function, total]
     rule bigUintType
         => rustStructType
             ( #token("BigUint", "Identifier"):Identifier
@@ -87,6 +86,7 @@ module MX-RUST-MODULES-BIGUINT
             BigUintIdId |-> i32(BigUintId:MInt{32})
             ...
         </values>
+
 endmodule
 
 ```

mx-rust-semantics/main/modules/call-value.md

@@ -0,0 +1,61 @@
+```k
+
+module MX-RUST-MODULES-CALL-VALUE
+    imports private COMMON-K-CELL
+    imports private MX-COMMON-SYNTAX
+    imports private MX-RUST-REPRESENTATION
+    imports private MX-RUST-REPRESENTATION-CONVERSIONS
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-SHARED-SYNTAX
+
+    syntax Identifier ::= "MxRust#CallValue"  [token]
+
+    syntax MxRustStructType ::= "callValueType"  [function, total]
+    rule callValueType
+        => rustStructType
+            ( MxRust#CallValue
+            , .MxRustStructFields
+            )
+
+    rule
+        normalizedMethodCall
+            ( MxRust#CallValue
+            , #token("new", "Identifier"):Identifier
+            , .PtrList
+            )
+        =>  mxRustNewStruct
+                ( callValueType
+                , .CallParamsList
+                )
+
+    rule
+        normalizedMethodCall
+            ( MxRust#CallValue
+            , #token("single_fungible_esdt", "Identifier"):Identifier
+            ,   ( ptr(_SelfId:Int)
+                , .PtrList
+                )
+            )
+        => MX#managedGetMultiESDTCallValue(.MxValueList)
+            ~> getSingleEsdt
+            ~> mxToRustTyped((str, #token("BigUint", "Identifier")))
+
+    syntax MxRustInstruction ::= "getSingleEsdt"
+
+    rule .MxEsdtTransferList ~> getSingleEsdt => #exception(UserError, "incorrect number of ESDT transfers")
+    rule _, _, _:MxEsdtTransferList ~> getSingleEsdt => #exception(UserError, "incorrect number of ESDT transfers")
+    rule    ( mxTransferValue(... token: _:String, nonce: Nonce:Int, value: _:Int)
+                , .MxEsdtTransferList
+            ~> getSingleEsdt
+            )
+        => #exception(UserError, "fungible ESDT token expected")
+        requires Nonce =/=Int 0
+    rule    ( mxTransferValue(... token: TokenId:String, nonce: 0, value: Value:Int)
+                , .MxEsdtTransferList
+            ~> getSingleEsdt
+            )
+        => mxListValue(mxStringValue(TokenId), mxIntValue(Value))
+
+endmodule
+
+```

mx-rust-semantics/main/preprocessing/contract.md

@@ -5,42 +5,70 @@ module MX-RUST-PREPROCESSING-CONTRACT
     imports MX-RUST-REPRESENTATION
     imports RUST-PREPROCESSING-CONFIGURATION
 
-    syntax MxRustInstruction ::= rustMxAddContractSend(TypePath)
+    syntax MxRustInstruction  ::= rustMxAddContractSend(TypePath)
+                                | rustMxAddContractCallValue(TypePath)
+                                | rustMxAddContractGenericMethod
+                                    ( trait: TypePath
+                                    , method: Identifier
+                                    , struct: Identifier
+                                    )
 
     rule rustMxAddContractMethods(Trait:TypePath)
         => rustMxAddContractSend(Trait:TypePath)
+            ~> rustMxAddContractCallValue(Trait:TypePath)
+
+    rule rustMxAddContractSend(Trait:TypePath)
+        => rustMxAddContractGenericMethod
+            (... trait: Trait
+            , method: #token("send", "Identifier")
+            , struct: #token("MxRust#Send", "Identifier")
+            )
+
+    rule rustMxAddContractCallValue(Trait:TypePath)
+        => rustMxAddContractGenericMethod
+            (... trait: Trait
+            , method: #token("call_value", "Identifier")
+            , struct: #token("MxRust#CallValue", "Identifier")
+            )
 
     rule
         <k>
-            rustMxAddContractSend(Trait:TypePath)
+            rustMxAddContractGenericMethod
+                (... trait: Trait:TypePath
+                , method: Method:Identifier
+                )
             => error
                 ( "send already exists for trait"
                 , ListItem(Trait)
                 )
             ...
         </k>
         <trait-path> Trait </trait-path>
-        <method-name> #token("send", "Identifier") </method-name>
+        <method-name> Method </method-name>
         [priority(50)]
 
     rule
         <k>
-            rustMxAddContractSend(Trait:TypePath)
+            rustMxAddContractGenericMethod
+                (... trait: Trait:TypePath
+                , method: Method:Identifier
+                , struct: Struct:Identifier
+                )
             => .K
             ...
         </k>
         <trait-path> Trait </trait-path>
         ( .Bag
             =>  <method>
-                    <method-name> #token("send", "Identifier") </method-name>
+                    <method-name> Method </method-name>
                     <method-params> self : $selftype , .NormalizedFunctionParameterList </method-params>
                     <method-return-type> #token("MxRust#CallReturnType", "Identifier") </method-return-type>
                     <method-implementation>
                         block({
                             .InnerAttributes
                             (
                                 (
-                                    (  #token("MxRust#Send", "Identifier")
+                                    (  Struct
                                     :: (#token("new", "Identifier"):PathExprSegment)
                                     :: .PathExprSegments
                                     )

mx-rust-semantics/main/representation.md

@@ -20,6 +20,7 @@ module MX-RUST-REPRESENTATION
                                 | mxRustNewValue(ValueOrError)
                                 | mxRustEmptyValue(MxRustType)
                                 | mxValueToRust(Type)
+                                // TODO: Replace with mxToRustTyped
                                 | mxValueToRust(Type, MxValue)
                                 | "rustValueToMx"
                                 | rustValueToMx(Value)
@@ -32,9 +33,11 @@ module MX-RUST-REPRESENTATION
                                 | "mxRustCheckMxStatus"
 
     syntax TraitType ::= "contract" | "proxy"
-    syntax MxRustType ::= "noType" | rustType(Type)
+    syntax MxRustType ::= "noType"
+                        | rustType(Type)
     syntax MxRustTypeOrError ::= MxRustType | SemanticsError
     syntax Value ::= MxRustType
+    syntax Type ::= "bigUintType"  [function, total]
 
     syntax MxOrRustValueOrInstruction ::= MxOrRustValue | MxRustInstruction
 
@@ -61,8 +64,8 @@ module MX-RUST-REPRESENTATION-CONVERSIONS
     syntax MxRustStructField ::= mxRustStructField(Identifier, MxRustType)
     syntax MxRustStructFields ::= List{MxRustStructField, ","}
     syntax MxRustStructType ::= rustStructType(TypePath, MxRustStructFields)
+    syntax Type ::= MxRustStructType
     syntax MxRustType ::= Type  // TODO: Remove and use `rustType(_)`
-                        | MxRustStructType
 
     syntax MxRustFieldValue ::= mxToRustField(Identifier, MxToRust)  [strict(2)]
     syntax MxRustFieldValueOrError ::= MxRustFieldValue | SemanticsError
@@ -71,10 +74,15 @@ module MX-RUST-REPRESENTATION-CONVERSIONS
     syntax MxToRustIntermediate ::= mxToRustStruct(structName:TypePath, MxRustFieldValues)
                                     [strict(2), result(MxToRustFieldValue)]
 
+    syntax MxToRustIntermediate ::= mxToRustTuple(MxToRustList)
+                                    [strict, result(MxToRustValue)]
+
     syntax MxToRust ::= mxToRustTyped(MxRustType, MxValue)
                       | MxValue
                       | PtrValue
                       | SemanticsError
+    syntax MxToRustOrError ::= MxToRust | SemanticsError
+    syntax MxToRustList ::= List{MxToRustOrError, ","}
 
     syntax MxOrRustValue ::= MxValue | Value
     syntax MxOrRustValueList ::= List{MxOrRustValue, ","}

mx-semantics/main/calls/hooks.md

@@ -66,6 +66,13 @@ module MX-CALLS-HOOKS
             )
 
     rule MX#finish ( V:MxValue ) => returnCallData(V)
+
+    rule
+        <k>
+            MX#managedGetMultiESDTCallValue(.MxValueList) => Transfers
+            ...
+        </k>
+        <mx-esdt-transfers> Transfers:MxEsdtTransferList </mx-esdt-transfers>
 endmodule
 
 ```

rust-semantics/error.md

@@ -10,6 +10,7 @@ module RUST-ERROR-SYNTAX
     syntax TypePathOrError ::= injectOrError(TypePathSegmentsOrError) [function, total]
     syntax TypePathSegmentsOrError ::= concat(TypePathSegment, TypePathSegmentsOrError)  [function, total]
     syntax ExpressionOrError ::= andOrError(ExpressionOrError, ExpressionOrError)  [function, total]
+    syntax ValueOrError ::= tupleOrError(ValueListOrError)  [function, total]
 endmodule
 
 module RUST-ERROR
@@ -40,6 +41,9 @@ module RUST-ERROR
     rule andOrError(_:ExpressionOrError, E:SemanticsError) => E
     rule andOrError(E:SemanticsError, _:Expression) => E
     rule andOrError(E1:Expression, E2:Expression) => E1 && E2
+
+    rule tupleOrError(L:ValueList) => tuple(L)
+    rule tupleOrError(E:SemanticsError) => E
 endmodule
 
 ```

rust-semantics/expression/casts.md

@@ -36,8 +36,11 @@ module RUST-CASTS
     rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
     rule implicitCast(V:Bool, bool) => V
+    rule implicitCast(S:String, str) => S
 
     rule implicitCast(tuple(.ValueList) #as V, ():Type) => V
+    rule implicitCast(tuple(Vs:ValueList), (Ts:NonEmptyTypeCsv))
+        => tupleOrError(implicitCastList(Vs, Ts))
 
     rule implicitCast(struct(T, _) #as V, T) => V
     rule implicitCast(struct(T, _) #as V, T < _ >) => V
@@ -48,6 +51,14 @@ module RUST-CASTS
     // We don't need a value for the unit type
     rule implicitCastTo(( )) => .K
 
+    syntax ValueListOrError ::= implicitCastList(ValueList, NonEmptyTypeCsv)  [function, total]
+    rule implicitCastList(V:Value , .ValueList, T:Type) => concat(implicitCast(V, T), .ValueList)
+    rule implicitCastList(V:Value , Vs:ValueList, T:Type, Ts:NonEmptyTypeCsv)
+        => concat(implicitCast(V, T), implicitCastList(Vs, Ts))
+    rule implicitCastList(Vs:ValueList, Ts:NonEmptyTypeCsv)
+        => error("implicitCastList values not paired with types", ListItem(Vs) ListItem(Ts))
+        [owise]
+
 endmodule
 
 ```

tests/mx-rust-contracts/call-value.1.run

@@ -0,0 +1,14 @@
+setBalance("Owner", "MyToken", 0, 1234);
+setCallee("Owner");
+
+push mxListValue();
+push mxStringValue("getTransfer");
+push mxIntValue(0);
+push mxTransfersValue(mxTransferValue("MyToken", 0, 10));
+push mxIntValue(0);
+push mxStringValue("TestContract");
+call 6 MX#managedExecuteOnDestContext;
+check_eq mxIntValue(0);
+
+push_return_value;
+check_eq mxListValue( mxStringValue("MyToken") , mxIntValue(10))