Implement MultiEncodedVec

mx-rust-semantics/main/modules.md

@@ -6,6 +6,7 @@ requires "modules/blockchain.md"
 requires "modules/call-value.md"
 requires "modules/hooks.md"
 requires "modules/managed-vec.md"
+requires "modules/multi-value-encoded.md"
 requires "modules/proxy.md"
 requires "modules/send.md"
 requires "modules/storage.md"
@@ -18,6 +19,7 @@ module MX-RUST-MODULES
     imports private MX-RUST-MODULES-CALL-VALUE
     imports private MX-RUST-MODULES-HOOKS
     imports private MX-RUST-MODULES-MANAGED-VEC
+    imports private MX-RUST-MODULES-MULTI-VALUE-ENCODED
     imports private MX-RUST-MODULES-PROXY
     imports private MX-RUST-MODULES-SEND
     imports private MX-RUST-MODULES-STORAGE

mx-rust-semantics/main/modules/managed-vec.md

@@ -81,6 +81,14 @@ module MX-RUST-MODULES-MANAGED-VEC
             ~> clearValue
             ~> ptrValue(null, tuple(.ValueList))
 
+    rule
+        normalizedMethodCall
+            ( #token("ManagedVec", "Identifier"):Identifier
+            , #token("into", "Identifier"):Identifier
+            , ( ptr(SelfId) , .PtrList)
+            )
+        => into(ptr(SelfId))
+
   // --------------------------------------
 
     syntax MxRustType ::= "managedVecType"  [function, total]
@@ -102,7 +110,7 @@ module MX-RUST-MODULES-MANAGED-VEC
     rule mxRustEmptyValue(rustType(#token("ManagedVec", "Identifier")))
         => mxToRustTyped
             ( managedVecType
-            , mxListValue(mxUnitValue() , mxRustType(()) , .MxValueList)
+            , mxListValue(mxListValue(.MxValueList) , mxRustType(()) , .MxValueList)
             )
 
     rule mxValueToRust(#token("ManagedVec", "Identifier"), V:MxValue)
@@ -144,6 +152,25 @@ module MX-RUST-MODULES-MANAGED-VEC
             ...
         </values>
         [priority(20), label(xyzzy)]
+
+  // --------------------------------------
+
+    syntax MxRustInstruction ::= into(Expression)  [strict]
+
+    rule into
+            ( ptrValue
+                ( _
+                , struct
+                    ( _
+                    ,   ( #token("mx_buffer_id", "Identifier"):Identifier |-> _
+                            #token("value_type", "Identifier"):Identifier |-> _
+                            .Map
+                        ) #as M:Map
+                    )
+                )
+            )
+        => ptrValue(null, struct(#token("MultiValueEncoded", "Identifier"):Identifier , M))
+
 endmodule
 
 ```

mx-rust-semantics/main/modules/multi-value-encoded.md

@@ -0,0 +1,73 @@
+```k
+
+module MX-RUST-MODULES-MULTI-VALUE-ENCODED
+    imports private MX-RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+
+    syntax MxRustInstruction ::= toVec(Expression)  [strict]
+
+    rule
+        normalizedMethodCall
+            ( #token("MultiValueEncoded", "Identifier"):Identifier
+            , #token("to_vec", "Identifier"):Identifier
+            , ( ptr(SelfId) , .PtrList)
+            )
+        => toVec(ptr(SelfId))
+
+    rule toVec
+            ( ptrValue
+                ( _
+                , struct
+                    ( _
+                    ,   ( #token("mx_buffer_id", "Identifier"):Identifier |-> _
+                            #token("value_type", "Identifier"):Identifier |-> _
+                            .Map
+                        ) #as M:Map
+                    )
+                )
+            )
+        => ptrValue(null, struct(#token("ManagedVec", "Identifier"):Identifier , M))
+
+  // --------------------------------------
+
+    syntax MxRustType ::= "multiValueEncodedType"  [function, total]
+    rule multiValueEncodedType
+        => rustStructType
+            ( #token("MultiValueEncoded", "Identifier"):Identifier
+            ,   ( mxRustStructField
+                    ( #token("mx_buffer_id", "Identifier"):Identifier
+                    , MxRust#buffer
+                    )
+                , mxRustStructField
+                    ( #token("value_type", "Identifier"):Identifier
+                    , MxRust#Type
+                    )
+                , .MxRustStructFields
+                )
+            )
+
+    rule mxValueToRust
+            ( #token("MultiValueEncoded", "Identifier") < ValueType:Type , .GenericArgList >
+            , V:MxValue
+            )
+        => mxToRustTyped(multiValueEncodedType, mxListValue(V , mxRustType(ValueType) , .MxValueList))
+
+    rule rustValueToMx
+            ( struct
+                ( #token("MultiValueEncoded", "Identifier"):Identifier
+                , #token("mx_buffer_id", "Identifier"):Identifier |-> VecValueId:Int
+                  #token("value_type", "Identifier"):Identifier |-> _:Int
+                  .Map
+                )
+            )
+        => mxRustGetBuffer(ptr(VecValueId))
+
+    syntax MxRustInstruction ::= mxRustGetBuffer(Expression)  [strict]
+    rule mxRustGetBuffer(ptrValue(_, i32(BufferId:MInt{32})))
+        => mxGetBuffer(MInt2Unsigned(BufferId))
+
+  // --------------------------------------
+
+endmodule
+
+```

mx-semantics/main/biguint/tools.md

@@ -5,11 +5,6 @@ module MX-BIGUINT-TOOLS
     imports private MX-BIGUINT-CONFIGURATION
     imports private MX-COMMON-SYNTAX
 
-    rule
-        <k> clearBigInts => .K ... </k>
-        <bigIntHeap> _ => .Map </bigIntHeap>
-        <bigIntHeapNextId> _ => 0 </bigIntHeapNextId>
-
     rule
         <k> mxGetBigInt(IntId:Int) => mxIntValue(V) ... </k>
         <bigIntHeap> IntId |-> V:Int ... </bigIntHeap>

mx-semantics/main/buffers/hooks.md

@@ -20,8 +20,8 @@ module MX-BUFFERS-HOOKS
 
  // extern int32_t   mBufferNewFromBytes(void* context, int32_t dataOffset, int32_t dataLength);
     rule
-        <k> MX#mBufferNewFromValue(V:MxValue, .MxValueList) => mxIntValue(NextId) ... </k>
-        <buffer-heap> Values:Map => Values[NextId <- mxListValue(V, .MxValueList)] </buffer-heap>
+        <k> MX#mBufferNewFromValue((mxListValue(_) #as V:MxValue), .MxValueList) => mxIntValue(NextId) ... </k>
+        <buffer-heap> Values:Map => Values[NextId <- V] </buffer-heap>
         <buffer-heap-next-id> NextId => NextId +Int 1 </buffer-heap-next-id>
 
  // extern int32_t   mBufferSetBytes(void* context, int32_t mBufferHandle, int32_t dataOffset, int32_t dataLength);

mx-semantics/main/buffers/tools.md

@@ -0,0 +1,13 @@
+```k
+
+module MX-BUFFER-TOOLS
+    imports private COMMON-K-CELL
+    imports private MX-BUFFERS-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+
+    rule
+        <k> mxGetBuffer(BufferId:Int) => V ... </k>
+        <buffer-heap> BufferId |-> V:MxValue ... </buffer-heap>
+endmodule
+
+```

mx-semantics/main/call-state/configuration.md

@@ -13,8 +13,10 @@ module MX-CALL-STATE-CONFIGURATION
         <mx-call-state>
             <mx-call-data/>
             <mx-return-values/>
-            <mx-biguint/>
-            <mx-buffers/>
+            <mx-internal-state>
+                <mx-biguint/>
+                <mx-buffers/>
+            </mx-internal-state>
         </mx-call-state>
 endmodule
 

mx-semantics/main/call-state/tools.md

@@ -34,6 +34,18 @@ module MX-CALL-STATE-TOOLS
                 </mx-call-state>
         )
 
+    rule
+        <k> clearMxInternalState => .K ... </k>
+        (_:MxInternalStateCell =>
+            <mx-internal-state>
+                <mx-biguint>
+                    <bigIntHeapNextId> 0 </bigIntHeapNextId>
+                    ...
+                </mx-biguint>
+                ...
+            </mx-internal-state>
+        )
+
 endmodule
 
 ```

mx-semantics/main/calls/tools.md

@@ -360,7 +360,7 @@ module MX-CALLS-TOOLS
                 (... function: FunctionName:String
                 , callData: CallData:MxCallDataCell
                 )
-            => clearBigInts ~> host.mkCall(FunctionName)
+            => clearMxInternalState ~> host.mkCall(FunctionName)
             ...
         </k>
         (_:MxCallDataCell => CallData)

mx-semantics/main/mx-common.md

@@ -9,6 +9,7 @@ requires "biguint/hooks.md"
 requires "biguint/tools.md"
 requires "blocks/hooks.md"
 requires "buffers/hooks.md"
+requires "buffers/tools.md"
 requires "call-state/tools.md"
 requires "calls/hooks.md"
 requires "calls/tools.md"
@@ -22,6 +23,7 @@ module MX-COMMON
     imports private MX-ACCOUNTS-TOOLS
     imports private MX-BIGUINT-HOOKS
     imports private MX-BIGUINT-TOOLS
+    imports private MX-BUFFER-TOOLS
     imports private MX-BLOCKS-HOOKS
     imports private MX-BUFFERS-HOOKS
     imports private MX-CALL-STATE-TOOLS

mx-semantics/main/syntax.md

@@ -50,7 +50,7 @@ module MX-COMMON-SYNTAX
                             | "pushWorldState"  [symbol(pushWorldState)]
                             | "dropWorldState"  [symbol(dropWorldState)]
                             | "popWorldState"  [symbol(popWorldState)]
-                            | "clearBigInts"  [symbol(clearBigInts)]
+                            | "clearMxInternalState"  [symbol(clearMxInternalState)]
                             | "endCall"  [symbol(endCall)]
                             | "finishExecuteOnDestContext"  [symbol(finishExecuteOnDestContext)]
                             | processBuiltinFunction(BuiltinFunction, String, String, MxCallDataCell)
@@ -60,6 +60,7 @@ module MX-COMMON-SYNTAX
                             | storeHostValue(destination: MxValue, value: MxValue)
                             | returnCallData(MxValue)  [symbol(returnCallData)]
                             | mxGetBigInt(Int)  [symbol(mxGetBigInt)]
+                            | mxGetBuffer(Int)  [symbol(mxGetBuffer)]
                             | callContract(function: String, input: MxCallDataCell )
                               [symbol(callContractString)]
 

rust-semantics/helpers.md

@@ -17,5 +17,7 @@ module RUST-HELPERS
     rule isSameType(i32(_), i32) => true
     rule isSameType(u32(_), u32) => true
     rule isSameType(struct(T, _), T:Type) => true
+    rule isSameType(struct(T, _), T:Identifier _:GenericArgs ) => true
+
 endmodule
 ```

tests/mx-rust-contracts/multi-value-encoded.1.run

@@ -0,0 +1,13 @@
+setCallee("Owner");
+
+push mxListValue(mxListValue(mxIntValue(123), mxIntValue(456)), mxIntValue(1));
+push mxStringValue("toVecGet");
+push mxIntValue(0);
+push mxTransfersValue();
+push mxIntValue(0);
+push mxStringValue("TestContract");
+call 6 MX#managedExecuteOnDestContext;
+check_eq mxIntValue(0);
+
+push_return_value;
+check_eq mxIntValue(456)

tests/mx-rust-contracts/multi-value-encoded.2.run

@@ -0,0 +1,13 @@
+setCallee("Owner");
+
+push mxListValue(mxIntValue(123), mxIntValue(456));
+push mxStringValue("intoMve");
+push mxIntValue(0);
+push mxTransfersValue();
+push mxIntValue(0);
+push mxStringValue("TestContract");
+call 6 MX#managedExecuteOnDestContext;
+check_eq mxIntValue(0);
+
+push_return_value;
+check_eq mxListValue(mxIntValue(123), mxIntValue(456))

tests/mx-rust-contracts/multi-value-encoded.rs

@@ -0,0 +1,27 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait Contract {
+    #[init]
+    fn init(&self) {}
+
+    #[upgrade]
+    fn upgrade(&self) {}
+
+    #[endpoint(toVecGet)]
+    fn to_vec_get(&self, v: MultiValueEncoded<BigUint>, idx: u64) -> BigUint {
+        let mut values:ManagedVec<BigUint> = v.to_vec();
+        values.get(idx)
+    }
+
+    #[endpoint(intoMve)]
+    fn into_mve(&self, a: u64, b:u64) -> MultiValueEncoded<BigUint> {
+        let mut values:ManagedVec<BigUint> = ManagedVec::new();
+        values.push(BigUint::from(a));
+        values.push(BigUint::from(b));
+        values.into()
+    }
+}