Rust <-> mx conversions

mx-rust-semantics/main/expression.md

@@ -1,8 +1,12 @@
 ```k
 
+requires "expression/mx-to-rust.md"
+requires "expression/rust-to-mx.md"
 requires "expression/strings.md"
 
 module MX-RUST-EXPRESSION
+    imports private MX-RUST-EXPRESSION-MX-TO-RUST
+    imports private MX-RUST-EXPRESSION-RUST-TO-MX
     imports private MX-RUST-EXPRESSION-STRINGS
 endmodule
 

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

@@ -0,0 +1,85 @@
+```k
+
+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-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)
+
+    syntax Bool ::= isMxToRustFieldValue(K)  [function, total, symbol(isMxToRustFieldValue)]
+    rule isMxToRustFieldValue(_:K) => false [owise]
+    rule isMxToRustFieldValue(_:PtrValue) => true
+    rule isMxToRustFieldValue(mxToRustField(_, V:MxToRust)) => isMxToRustValue(V)
+    rule isMxToRustFieldValue(.MxRustFieldValues) => true
+    rule isMxToRustFieldValue(A:MxRustFieldValue , As:MxRustFieldValues)
+        => isMxToRustFieldValue(A) andBool isMxToRustFieldValue(As)
+
+    rule V:MxValue ~> mxToRustTyped(T:Type) => mxToRustTyped(T, V)
+
+    rule mxToRustTyped(T:Type, mxIntValue(I:Int)) => mxRustNewValue(integerToValue(I, T))
+        requires
+            (T ==K i32 orBool T ==K u32)
+            orBool (T ==K i64 orBool T ==K u64)
+    rule mxToRustTyped(str, mxStringValue(S:String)) => mxRustNewValue(S)
+    rule mxToRustTyped
+            ( rustStructType(StructName:TypePath, Fields:MxRustStructFields)
+            , mxListValue(Values:MxValueList)
+            )
+        => mxToRustStruct(StructName, pairFields(Fields, Values))
+    rule mxToRustTyped(() , mxUnitValue()) => ptrValue(null, tuple(.ValueList))
+
+    context HOLE:MxRustFieldValue , _:MxRustFieldValues [result(MxToRustFieldValue)]
+    context V:MxRustFieldValue , HOLE:MxRustFieldValues requires isMxToRustFieldValue(V)
+        [result(MxToRustFieldValue)]
+
+    syntax MxRustFieldValues ::= pairFields(MxRustStructFields, MxValueList)  [function, total]
+    rule pairFields(.MxRustStructFields, .MxValueList) => .MxRustFieldValues
+    rule pairFields
+            ( (mxRustStructField(Name:Identifier, T:MxRustType) , Fs:MxRustStructFields)
+            , (V:MxValue , Vs:MxValueList)
+            )
+        => mxToRustField(Name, mxToRustTyped(T, V)) , pairFields(Fs, Vs)
+    rule pairFields(.MxRustStructFields, (_:MxValue , _:MxValueList) #as L:MxValueList)
+        => error("Not enough fields", ListItem(L))
+    rule pairFields((_ , _:MxRustStructFields) #as F, .MxValueList)
+        => error("Not enough values", ListItem(F))
+    rule pairFields(F:MxRustStructFields, V:MxValueList)
+        => error("Should not happen (pairFields)", ListItem(F) ListItem(V))
+        [owise]
+
+    rule (.K => fieldsToMap(Fields, .Map))
+        ~> mxToRustStruct(_StructName:TypePath, Fields:MxRustFieldValues)
+        requires isMxToRustFieldValue(Fields)
+
+    rule M:Map ~>  mxToRustStruct(StructName:TypePath, _Fields:MxRustFieldValues)
+        => mxRustNewValue(struct(StructName, M))
+
+    syntax MapOrError ::= fieldsToMap(MxRustFieldValues, Map)  [function, total]
+    rule fieldsToMap(.MxRustFieldValues, M:Map) => M
+    rule fieldsToMap
+            ( mxToRustField(Name:Identifier, ptrValue(ptr(I:Int), _:Value))
+                , Fields:MxRustFieldValues
+            , M
+            )
+        => fieldsToMap(Fields, M[Name <- I])
+        requires notBool Name in_keys(M)
+    rule fieldsToMap
+            (   ( (mxToRustField(Name:Identifier, _) #as Field:MxRustFieldValue)
+                , _Fields:MxRustFieldValues
+                )
+            , M
+            )
+        => error("Field name already in map", ListItem(Field) ListItem(M))
+        requires Name in_keys(M)
+    rule fieldsToMap((Field , _:MxRustFieldValues), _:Map)
+        => error("Unexpected field", ListItem(Field))
+        [owise]
+endmodule
+
+```

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

@@ -0,0 +1,37 @@
+```k
+
+module MX-RUST-EXPRESSION-RUST-TO-MX
+    imports private COMMON-K-CELL
+    imports private K-EQUAL-SYNTAX
+    imports private LIST
+    imports private MAP
+    imports private MX-COMMON-SYNTAX
+    imports private MX-RUST-REPRESENTATION-CONVERSIONS
+    imports private RUST-CONVERSIONS-SYNTAX
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-REPRESENTATION
+
+    rule V:MxValue ~> rustToMx => rustToMx(V)
+
+    rule
+        <k>
+            rustToMx(struct (_, Fields:Map))
+            => rustValuesToMxListValue
+                ( ptrListToValueList(listToPtrList(values(Fields)), Values)
+                , .MxValueList
+                )
+            ...
+        </k>
+        <values> Values:Map </values>
+        [priority(200)]
+    rule rustToMx(S:String => mxStringValue(S))
+    rule rustToMx(tuple(V:ValueList)) => rustValuesToMxListValue(V, .MxValueList)
+
+    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)
+    rule (rustToMx(HOLE:MxValue) => .K) ~> rustValuesToMxListValue(_:ValueList, (L:MxValueList => (HOLE, L)))
+endmodule
+
+```

mx-rust-semantics/main/representation.md

@@ -2,6 +2,7 @@
 
 module MX-RUST-REPRESENTATION
     imports MX-COMMON-SYNTAX
+    imports MX-RUST-REPRESENTATION-CONVERSIONS
     imports RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
 
@@ -38,4 +39,36 @@ module MX-RUST-REPRESENTATION
     syntax ContractCode ::= rustCode(MxRustPreprocessedCell,  PreprocessedCell)
 endmodule
 
+module MX-RUST-REPRESENTATION-CONVERSIONS
+    imports MX-COMMON-SYNTAX
+    imports RUST-SHARED-SYNTAX
+    imports RUST-VALUE-SYNTAX
+
+    syntax MxRustStructField ::= mxRustStructField(Identifier, MxRustType)
+    syntax MxRustStructFields ::= List{MxRustStructField, ","}
+    syntax MxRustStructType ::= rustStructType(TypePath, MxRustStructFields)
+    syntax MxRustType ::= Type  // TODO: Remove and use `rustType(_)`
+                        | MxRustStructType
+
+    syntax MxRustFieldValue ::= mxToRustField(Identifier, MxToRust)  [strict(2)]
+    syntax MxRustFieldValueOrError ::= MxRustFieldValue | SemanticsError
+    syntax MxRustFieldValues ::= List{MxRustFieldValueOrError, ","}
+
+    syntax MxToRustIntermediate ::= mxToRustStruct(structName:TypePath, MxRustFieldValues)
+                                    [strict(2), result(MxToRustFieldValue)]
+
+    syntax MxToRust ::= mxToRustTyped(MxRustType, MxValue)
+                      | MxValue
+                      | PtrValue
+                      | SemanticsError
+
+    syntax MxOrRustValue ::= MxValue | Value
+    syntax MxOrRustValueList ::= List{MxOrRustValue, ","}
+    syntax MxOrRustValueListOrError ::= MxOrRustValueList | SemanticsError
+    syntax MxRustInstruction ::= mxToRustTyped(MxRustType)
+
+    syntax MxRustInstruction  ::= rustToMx(MxOrRustValue)
+                                | "rustToMx"
+endmodule
+
 ```

rust-semantics/conversions.md

@@ -0,0 +1,32 @@
+```k
+
+module RUST-CONVERSIONS-SYNTAX
+    imports LIST
+    imports RUST-REPRESENTATION
+
+    syntax PtrListOrError ::= listToPtrList(List)  [function, total]
+    syntax ValueListOrError ::= ptrListToValueList(PtrListOrError, Map)  [function, total]
+endmodule
+
+module RUST-CONVERSIONS
+    imports private RUST-CONVERSIONS-SYNTAX
+    imports private RUST-ERROR-SYNTAX
+
+    rule listToPtrList(.List) => .PtrList
+    rule listToPtrList(ListItem(P:Int) L:List) => concat(ptr(P), listToPtrList(L))
+    rule listToPtrList(L:List) => error("Unrecognized element (listToPtrList)", L)
+        [owise]
+
+    rule ptrListToValueList(E:SemanticsError, _:Map) => E
+    rule ptrListToValueList(.PtrList, _:Map) => .ValueList
+    rule ptrListToValueList((ptr(P:Int) , Ps:PtrList), M:Map)
+        => concat({M[P:Int:KItem]}:>Value, ptrListToValueList(Ps, M:Map))
+        requires P:Int:KItem in_keys(M) andBool isValue(M[P:Int:KItem] orDefault 0)
+        [preserves-definedness]
+    rule ptrListToValueList(Ps:PtrList, M:Map)
+        => error("element not in map or wrong value type (ptrListToValueList)", ListItem(Ps) ListItem(M))
+        [owise]
+
+endmodule
+
+```

rust-semantics/error.md

@@ -1,14 +1,28 @@
 ```k
 
+module RUST-ERROR-SYNTAX
+    imports RUST-REPRESENTATION
+
+    syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError)  [function, total]
+    syntax PtrListOrError ::= concat(Ptr, PtrListOrError)  [function, total]
+    syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError)  [function, total]
+endmodule
+
 module RUST-ERROR
-    imports private RUST-REPRESENTATION
+    imports private RUST-ERROR-SYNTAX
+
+    rule concat(P:Ptr, L:PtrList) => P , L
+    rule concat(_:Ptr, E:SemanticsError) => E
 
     rule concat(V:Value, L:ValueList) => V , L
     rule concat(_:Value, E:SemanticsError) => E
     rule concat(E:SemanticsError, _:ValueListOrError) => E
     rule concat(E:ValueOrError, L:ValueListOrError)
         => error("unexpected branch (concat(ValueOrError, ValueListOrError))", ListItem(E) ListItem(L))
         [owise]
+
+    rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V)
+    rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E
 endmodule
 
-```
+```

rust-semantics/expression/casts.md

@@ -1,6 +1,7 @@
 ```k
 
 module RUST-CASTS
+    imports private RUST-ERROR-SYNTAX
     imports private RUST-REPRESENTATION
 
     syntax ValueOrError ::= implicitCast(Value, Type)  [function, total]

rust-semantics/expression/expression-list.md

@@ -1,8 +1,9 @@
 ```k
 
 module RUST-EXPRESSION-EXPRESSION-LIST
-    imports RUST-REPRESENTATION
-    imports RUST-VALUE-SYNTAX
+    imports private RUST-ERROR-SYNTAX
+    imports private RUST-REPRESENTATION
+    imports private RUST-VALUE-SYNTAX
 
     rule evaluate(L:ExpressionList) => evaluate(expressionListToValueList(L))
 

rust-semantics/expression/literals.md

@@ -4,12 +4,13 @@ module RUST-EXPRESSION-LITERALS
 endmodule
 
 module RUST-EXPRESSION-INTEGER-LITERALS
-    imports BOOL
-    imports INT
-    imports K-EQUAL-SYNTAX
-    imports STRING
+    imports private BOOL
+    imports private INT
+    imports private K-EQUAL-SYNTAX
+    imports private STRING
+    imports private RUST-ERROR-SYNTAX
     imports private RUST-REPRESENTATION
-    imports RUST-SHARED-SYNTAX
+    imports private RUST-SHARED-SYNTAX
 
     // https://doc.rust-lang.org/stable/reference/expressions/literal-expr.html#integer-literal-expressions
     // https://doc.rust-lang.org/stable/reference/tokens.html#number-literals

rust-semantics/representation.md

@@ -30,7 +30,6 @@ module RUST-VALUE-SYNTAX
     syntax ValueOrError ::= Value | SemanticsError
 
     syntax ValueListOrError ::= ValueList | SemanticsError
-    syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError)  [function, total]
 
     syntax Ptr ::= "null" | ptr(Int)
     syntax PtrValue ::= ptrValue(Ptr, Value)
@@ -39,10 +38,6 @@ module RUST-VALUE-SYNTAX
     syntax Expression ::= PtrValue
     syntax KResult ::= PtrValue
 
-    syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError)  [function, total]
-    rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V)
-    rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E
-
     syntax Bool ::= mayBeDefaultTypedInt(Value)  [function, total]
     rule mayBeDefaultTypedInt(_V) => false  [owise]
     rule mayBeDefaultTypedInt(u128(_)) => true
@@ -61,6 +56,7 @@ module RUST-REPRESENTATION
     syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","}
 
     syntax PtrList ::=List{Ptr, ","}
+    syntax PtrListOrError ::= PtrList | SemanticsError
 
     syntax Instruction  ::= normalizedMethodCall(TypePath, Identifier, PtrList)
                           | implicitCastTo(Type)
@@ -78,6 +74,8 @@ module RUST-REPRESENTATION
                             [strict(3), result(ValueWithPtr)]
                           | "Rust#newStruct" "(" type:TypePath "," fields:Map ")"
 
+    syntax MapOrError ::= Map | SemanticsError
+    
     syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
 
     syntax Type ::= "$selftype"
@@ -87,6 +85,7 @@ module RUST-REPRESENTATION
                         | "i64"  [token]
                         | "u64"  [token]
                         | "bool" [token]
+                        | "str"  [token]
                         
     syntax MaybeIdentifier ::= ".Identifier" | Identifier
 

rust-semantics/rust-common.md

@@ -1,5 +1,6 @@
 ```k
 requires "config.md"
+requires "conversions.md"
 requires "error.md"
 requires "execution.md"
 requires "expression.md"
@@ -9,6 +10,7 @@ requires "representation.md"
 requires "rust-common-syntax.md"
 
 module RUST-COMMON
+  imports RUST-CONVERSIONS
   imports RUST-ERROR
   imports RUST-EXECUTION
   imports RUST-EXPRESSION