Updating to match main (#109)

* Implement TokenIdentifier (#100) * Mutable variables (#105) * Update K to 149 (#99) (#101) Co-authored-by: Virgil <[email protected]> * Introducing mutable variables and preventing override on immutable ones * Adding minor comments * Update K to 149 (#99) (#104) Co-authored-by: Virgil <[email protected]> * Removing restrictions over reassignments of immutable variables * [Fix] Removing restrictions over reassignments of immutable variables * Addressing review comments --------- Co-authored-by: Virgil <[email protected]> * Implement the send() function for contracts (#102) * Enabling assignments on tuples with let expressions (#107) * Enabling assignments on tuples with let expressions * Addressing comments * Implement call_value() (#103) * BigUint operations (#106) --------- Co-authored-by: Virgil <[email protected]>
Pi-Squared-Inc · Sep 27, 2024 · 361abef · 361abef
1 parent bf17bc2
commit 361abef
Show file tree

Hide file tree

Showing 59 changed files with 1,286 additions and 118 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
 .build
 .DS_store
 tmp
+tmp.*
diff --git a/mx-rust-semantics/main/expression/mx-to-rust.md b/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
 
 ```
diff --git a/mx-rust-semantics/main/expression/rust-to-mx.md b/mx-rust-semantics/main/expression/rust-to-mx.md
@@ -24,10 +24,13 @@ 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(tuple(V:ValueList)) => rustValuesToMxListValue(V, .MxValueList)
+    rule rustToMx(V:Value => mxIntValue({valueToInteger(V)}:>Int))
+        requires notBool isSemanticsError(valueToInteger(V))
 
-    syntax RustMxInstruction ::= rustValuesToMxListValue(ValueListOrError, MxValueList)
     rule rustValuesToMxListValue(.ValueList, L:MxValueList)
         => rustToMx(mxListValue(reverse(L, .MxValueList)))
     rule (.K => rustToMx(HOLE)) ~> rustValuesToMxListValue(((HOLE:Value , V:ValueList) => V), _:MxValueList)

diff --git a/mx-rust-semantics/main/glue.md b/mx-rust-semantics/main/glue.md
@@ -56,17 +56,20 @@ module MX-RUST-GLUE
             (T ==K i32 orBool T ==K u32)
             orBool (T ==K i64 orBool T ==K u64)
 
-    rule
-        <k> ptr(I:Int) => ptrValue(ptr(I), V) ... </k>
-        <values> I |-> V:Value ... </values>
-
     rule ptrValue(_, V) ~> rustValueToMx => rustValueToMx(V)
 
-    rule rustValueToMx(tuple(.ValueList)) => mxUnitValue()
-    
-    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
+
+    rule (.K => rustValuesToMxListValue(Values, .MxValueList))
+        ~> rustMxCallHook(_, Values:ValueList)
+    rule (rustToMx(mxListValue(L:MxValueList)) ~> rustMxCallHook(Hook:MxHookName, _))
+        => Hook(L)
 
+    rule L:MxValue ~> mxRustWrapInMxList => mxListValue(L)
 endmodule
 
 ```
diff --git a/mx-rust-semantics/main/modules.md b/mx-rust-semantics/main/modules.md
@@ -2,16 +2,22 @@
 
 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"
 requires "modules/storage.md"
+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
     imports private MX-RUST-MODULES-STORAGE
+    imports private MX-RUST-MODULES-TOKEN-IDENTIFIER
 endmodule
 
 ```
diff --git a/mx-rust-semantics/main/modules/address.md b/mx-rust-semantics/main/modules/address.md
@@ -28,7 +28,7 @@ module MX-RUST-MODULES-ADDRESS
             ( struct
                 ( #token("ManagedAddress", "Identifier"):Identifier
                 , #token("mx_address_value", "Identifier"):Identifier |-> AddressValueId:Int
-                  _:Map
+                  .Map
                 )
             )
         => ptr(AddressValueId) ~> rustValueToMx

diff --git a/mx-rust-semantics/main/modules/biguint.md b/mx-rust-semantics/main/modules/biguint.md
@@ -3,6 +3,7 @@
 module MX-RUST-MODULES-BIGUINT
     imports private COMMON-K-CELL
     imports private MX-COMMON-SYNTAX
+    imports private MX-RUST-BIGUINT-OPERATORS
     imports private MX-RUST-REPRESENTATION
     imports private RUST-EXECUTION-CONFIGURATION
     imports private RUST-REPRESENTATION
@@ -25,9 +26,15 @@ module MX-RUST-MODULES-BIGUINT
         </k>
         <values> ValueId |-> V:Value ... </values>
 
+    rule normalizedMethodCall
+            ( #token("BigUint", "Identifier"):Identifier
+            , #token("zero", "Identifier"):Identifier
+            , .PtrList
+            )
+        => mxRustBigIntNew(0)
+
   // --------------------------------------
-    syntax MxRustType ::= "bigUintType"  [function, total]
-    rule bigUintType
+    rule bigUintFromValueType
         => rustStructType
             ( #token("BigUint", "Identifier"):Identifier
             ,   ( mxRustStructField
@@ -37,9 +44,19 @@ module MX-RUST-MODULES-BIGUINT
                 , .MxRustStructFields
                 )
             )
+    rule bigUintFromIdType
+        => rustStructType
+            ( #token("BigUint", "Identifier"):Identifier
+            ,   ( mxRustStructField
+                    ( #token("mx_biguint_id", "Identifier"):Identifier
+                    , i32
+                    )
+                , .MxRustStructFields
+                )
+            )
   // --------------------------------------
     rule mxToRustTyped(#token("BigUint", "Identifier"):Identifier, V:MxValue)
-        => mxToRustTyped(bigUintType, mxListValue(V))
+        => mxToRustTyped(bigUintFromValueType, mxListValue(V))
 
     rule (.K => MX#bigIntNew(mxIntValue(I)))
         ~> mxToRustTyped(MxRust#bigInt, mxIntValue(I:Int))
@@ -51,7 +68,7 @@ module MX-RUST-MODULES-BIGUINT
                                 | "mxRustCreateBigUint"
 
     rule mxRustBigIntNew(V:Int)
-        => mxToRustTyped(bigUintType, mxListValue(mxIntValue(V)))
+        => mxToRustTyped(bigUintFromValueType, mxListValue(mxIntValue(V)))
 
     rule mxRustEmptyValue(rustType(#token("BigUint", "Identifier")))
         => mxRustBigIntNew(0)
@@ -87,6 +104,163 @@ module MX-RUST-MODULES-BIGUINT
             BigUintIdId |-> i32(BigUintId:MInt{32})
             ...
         </values>
+
+endmodule
+
+module MX-RUST-BIGUINT-OPERATORS
+    imports private COMMON-K-CELL
+    imports private MX-RUST-REPRESENTATION
+    imports private RUST-EXECUTION-CONFIGURATION
+
+    syntax MxRustInstruction ::= rustMxBinaryBigUintOperator(MxHookName, Value, Value)
+    rule
+        <k>
+            rustMxBinaryBigUintOperator
+                ( Hook:MxHookName
+                , struct
+                    ( #token("BigUint", "Identifier"):Identifier #as BigUint:TypePath
+                    , #token("mx_biguint_id", "Identifier"):Identifier |-> FirstId:Int
+                      _:Map
+                    )
+                , struct
+                    ( #token("BigUint", "Identifier"):Identifier #as BigUint:TypePath
+                    , #token("mx_biguint_id", "Identifier"):Identifier |-> SecondId:Int
+                      _:Map
+                    )
+                )
+            => rustMxCallHook(Hook, (V1, V2, .ValueList))
+              ~> mxRustWrapInMxList
+              ~> mxToRustTyped(bigUintFromIdType)
+            ...
+        </k>
+        <values>
+            FirstId |-> V1:Value
+            SecondId |-> V2:Value
+            ...
+        </values>
+
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            + ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintOperator(MX#bigIntAdd, V1, V2)
+
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            - ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintOperator(MX#bigIntSub, V1, V2)
+
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            * ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintOperator(MX#bigIntMul, V1, V2)
+
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            / ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintOperator(MX#bigIntDiv, V1, V2)
+
+
+
+    rule
+        (ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
+            + (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
+        => V1 + bigUintFrom(V2)
+
+    rule
+        (ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
+            - (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
+        => V1 - bigUintFrom(V2)
+
+    rule
+        (ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
+            * (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
+        => V1 * bigUintFrom(V2)
+
+    rule
+        (ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
+            / (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
+        => V1 / bigUintFrom(V2)
+
+    syntax Expression ::= bigUintFrom(Expression)  [function, total]
+    rule bigUintFrom(V:Expression)
+        =>  ( #token("BigUint", "Identifier"):Identifier
+            :: #token("from", "Identifier"):Identifier
+            :: .PathExprSegments
+            )
+            ( V, .CallParamsList )
+
+
+    syntax MxRustInstruction ::= rustMxBinaryBigUintComparisonOperator(MxHookName, Value, Value)
+    rule
+        <k>
+            rustMxBinaryBigUintComparisonOperator
+                ( Hook:MxHookName
+                , struct
+                    ( #token("BigUint", "Identifier"):Identifier
+                    , #token("mx_biguint_id", "Identifier"):Identifier |-> FirstId:Int
+                      _:Map
+                    )
+                , struct
+                    ( #token("BigUint", "Identifier"):Identifier
+                    , #token("mx_biguint_id", "Identifier"):Identifier |-> SecondId:Int
+                      _:Map
+                    )
+                )
+            => rustMxCallHook(Hook, (V1, V2, .ValueList))
+              ~> mxToRustTyped(i32)
+            ...
+        </k>
+        <values>
+            FirstId |-> V1:Value
+            SecondId |-> V2:Value
+            ...
+        </values>
+
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            == ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
+            ~> mxRustEqResult
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            != ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
+            ~> mxRustNeResult
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            < ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)  // >
+        => rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
+            ~> mxRustLtResult
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            <= ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
+            ~> mxRustLeResult
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            > ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
+            ~> mxRustGtResult
+    rule
+        ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+            >= ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
+        => rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
+            ~> mxRustGeResult
+
+    syntax MxRustInstruction  ::= "mxRustEqResult"
+                                | "mxRustNeResult"
+                                | "mxRustGeResult"
+                                | "mxRustGtResult"
+                                | "mxRustLeResult"
+                                | "mxRustLtResult"
+
+    rule V:PtrValue ~> mxRustEqResult => V == ptrValue(null, i32(0p32))
+    rule V:PtrValue ~> mxRustNeResult => V != ptrValue(null, i32(0p32))
+    rule V:PtrValue ~> mxRustGeResult => V >= ptrValue(null, i32(0p32))
+    rule V:PtrValue ~> mxRustGtResult => V > ptrValue(null, i32(0p32))
+    rule V:PtrValue ~> mxRustLtResult => V < ptrValue(null, i32(0p32))  // >
+    rule V:PtrValue ~> mxRustLeResult => V <= ptrValue(null, i32(0p32))
+
 endmodule
 
 ```